Theorem xor2 671

Description: Two ways to express "exclusive or."

Assertion

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

Proof of Theorem xor2

Step	Hyp	Ref	Expression
1		xor 669	. 2 |- (-. (ph <-> ps) <-> ((ph /\ -. ps) \/ (ps /\ -. ph)))
2		ioran 306	. . 3 |- (-. ((ph /\ ps) \/ (-. ph /\ -. ps)) <-> (-. (ph /\ ps) /\ -. (-. ph /\ -. ps)))
3		pm5.24 670	. . 3 |- (-. ((ph /\ ps) \/ (-. ph /\ -. ps)) <-> ((ph /\ -. ps) \/ (ps /\ -. ph)))
4		oran 312	. . . . 5 |- ((ph \/ ps) <-> -. (-. ph /\ -. ps))
5	4	anbi2i 479	. . . 4 |- ((-. (ph /\ ps) /\ (ph \/ ps)) <-> (-. (ph /\ ps) /\ -. (-. ph /\ -. ps)))
6		ancom 435	. . . 4 |- ((-. (ph /\ ps) /\ (ph \/ ps)) <-> ((ph \/ ps) /\ -. (ph /\ ps)))
7	5, 6	bitr3 175	. . 3 |- ((-. (ph /\ ps) /\ -. (-. ph /\ -. ps)) <-> ((ph \/ ps) /\ -. (ph /\ ps)))
8	2, 3, 7	3bitr3 181	. 2 |- (((ph /\ -. ps) \/ (ps /\ -. ph)) <-> ((ph \/ ps) /\ -. (ph /\ ps)))
9	1, 8	bitr 173	1 |- (-. (ph <-> ps) <-> ((ph \/ ps) /\ -. (ph /\ ps)))

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

This theorem is referenced by:  nmogtmnf 8365  nmopgtmnf 9712

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