Theorem dfbi 499

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 497	. 2 |- ((ph <-> ps) <-> -. (ph <-> -. ps))
2		imnan 207	. . . . 5 |- ((ph -> -. ps) <-> -. (ph /\ ps))
3		bi2.15 145	. . . . . 6 |- ((-. ps -> ph) <-> (-. ph -> ps))
4		iman 205	. . . . . 6 |- ((-. ph -> ps) <-> -. (-. ph /\ -. ps))
5	3, 4	bitr 151	. . . . 5 |- ((-. ps -> ph) <-> -. (-. ph /\ -. ps))
6	2, 5	anbi12i 369	. . . 4 |- (((ph -> -. ps) /\ (-. ps -> ph)) <-> (-. (ph /\ ps) /\ -. (-. ph /\ -. ps)))
7		bi 396	. . . 4 |- ((ph <-> -. ps) <-> ((ph -> -. ps) /\ (-. ps -> ph)))
8		ioran 254	. . . 4 |- (-. ((ph /\ ps) \/ (-. ph /\ -. ps)) <-> (-. (ph /\ ps) /\ -. (-. ph /\ -. ps)))
9	6, 7, 8	3bitr4r 159	. . 3 |- (-. ((ph /\ ps) \/ (-. ph /\ -. ps)) <-> (ph <-> -. ps))
10	9	bicon1i 193	. 2 |- (-. (ph <-> -. ps) <-> ((ph /\ ps) \/ (-. ph /\ -. ps)))
11	1, 10	bitr 151	1 |- ((ph <-> ps) <-> ((ph /\ ps) \/ (-. ph /\ -. ps)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195   /\ wa 196

This theorem is referenced by:  xor 500  biass 511  symdif2 1690  ifbi 1783

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

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org