Theorem dfbi 669

Description: An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124.

Assertion

Ref	Expression
dfbi	|- ((ph <-> ps) <-> ((ph /\ ps) \/ (-. ph /\ -. ps)))

Proof of Theorem dfbi

Step	Hyp	Ref	Expression
1		pm5.18 659	. 2 |- ((ph <-> ps) <-> -. (ph <-> -. ps))
2		imnan 242	. . . . 5 |- ((ph -> -. ps) <-> -. (ph /\ ps))
3		bi2.15 166	. . . . . 6 |- ((-. ps -> ph) <-> (-. ph -> ps))
4		iman 237	. . . . . 6 |- ((-. ph -> ps) <-> -. (-. ph /\ -. ps))
5	3, 4	bitr 173	. . . . 5 |- ((-. ps -> ph) <-> -. (-. ph /\ -. ps))
6	2, 5	anbi12i 482	. . . 4 |- (((ph -> -. ps) /\ (-. ps -> ph)) <-> (-. (ph /\ ps) /\ -. (-. ph /\ -. ps)))
7		bi 514	. . . 4 |- ((ph <-> -. ps) <-> ((ph -> -. ps) /\ (-. ps -> ph)))
8		ioran 306	. . . 4 |- (-. ((ph /\ ps) \/ (-. ph /\ -. ps)) <-> (-. (ph /\ ps) /\ -. (-. ph /\ -. ps)))
9	6, 7, 8	3bitr4r 184	. . 3 |- (-. ((ph /\ ps) \/ (-. ph /\ -. ps)) <-> (ph <-> -. ps))
10	9	con1bii 220	. 2 |- (-. (ph <-> -. ps) <-> ((ph /\ ps) \/ (-. ph /\ -. ps)))
11	1, 10	bitr 173	1 |- ((ph <-> ps) <-> ((ph /\ ps) \/ (-. ph /\ -. ps)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223

This theorem is referenced by:  xor 670  pm5.24 671  symdif2 2263  ifbi 2368

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain