Theorem dfbi3 733

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

Assertion

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

Proof of Theorem dfbi3

Step	Hyp	Ref	Expression
1		pm5.18 722	. 2 |- ((ph <-> ps) <-> -. (ph <-> -. ps))
2		imnan 261	. . . . 5 |- ((ph -> -. ps) <-> -. (ph /\ ps))
3		con1b 181	. . . . . 6 |- ((-. ps -> ph) <-> (-. ph -> ps))
4		iman 256	. . . . . 6 |- ((-. ph -> ps) <-> -. (-. ph /\ -. ps))
5	3, 4	bitri 190	. . . . 5 |- ((-. ps -> ph) <-> -. (-. ph /\ -. ps))
6	2, 5	anbi12i 540	. . . 4 |- (((ph -> -. ps) /\ (-. ps -> ph)) <-> (-. (ph /\ ps) /\ -. (-. ph /\ -. ps)))
7		dfbi2 572	. . . 4 |- ((ph <-> -. ps) <-> ((ph -> -. ps) /\ (-. ps -> ph)))
8		ioran 331	. . . 4 |- (-. ((ph /\ ps) \/ (-. ph /\ -. ps)) <-> (-. (ph /\ ps) /\ -. (-. ph /\ -. ps)))
9	6, 7, 8	3bitr4ri 201	. . 3 |- (-. ((ph /\ ps) \/ (-. ph /\ -. ps)) <-> (ph <-> -. ps))
10	9	con1bii 237	. 2 |- (-. (ph <-> -. ps) <-> ((ph /\ ps) \/ (-. ph /\ -. ps)))
11	1, 10	bitri 190	1 |- ((ph <-> ps) <-> ((ph /\ ps) \/ (-. ph /\ -. ps)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240

This theorem is referenced by:  xor 734  pm5.24 735  nic-justbi 1234  symdif2OLD 2858  ifbi 2995

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 164  df-or 241  df-an 242

Copyright terms: Public domain