New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  xor GIF version

Theorem xor 861
 Description: Two ways to express "exclusive or." Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.)
Assertion
Ref Expression
xor (¬ (φψ) ↔ ((φ ¬ ψ) (ψ ¬ φ)))

Proof of Theorem xor
StepHypRef Expression
1 iman 413 . . . 4 ((φψ) ↔ ¬ (φ ¬ ψ))
2 iman 413 . . . 4 ((ψφ) ↔ ¬ (ψ ¬ φ))
31, 2anbi12i 678 . . 3 (((φψ) (ψφ)) ↔ (¬ (φ ¬ ψ) ¬ (ψ ¬ φ)))
4 dfbi2 609 . . 3 ((φψ) ↔ ((φψ) (ψφ)))
5 ioran 476 . . 3 (¬ ((φ ¬ ψ) (ψ ¬ φ)) ↔ (¬ (φ ¬ ψ) ¬ (ψ ¬ φ)))
63, 4, 53bitr4ri 269 . 2 (¬ ((φ ¬ ψ) (ψ ¬ φ)) ↔ (φψ))
76con1bii 321 1 (¬ (φψ) ↔ ((φ ¬ ψ) (ψ ¬ φ)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360 This theorem is referenced by:  dfbi3  863  pm5.24  864  4exmid  905  excxor  1309  elsymdif  3223  symdif2  3520
 Copyright terms: Public domain W3C validator