Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  excxor Structured version   GIF version

Theorem excxor 1268
 Description: This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010.) (Proof rewritten by Jim Kingdon, 5-May-2018.)
Assertion
Ref Expression
excxor ((φψ) ↔ ((φ ¬ ψ) φ ψ)))

Proof of Theorem excxor
StepHypRef Expression
1 xoranor 1267 . . 3 ((φψ) ↔ ((φ ψ) φ ¬ ψ)))
2 andi 730 . . 3 (((φ ψ) φ ¬ ψ)) ↔ (((φ ψ) ¬ φ) ((φ ψ) ¬ ψ)))
3 orcom 646 . . . . 5 (((ψ ¬ φ) (φ ¬ φ)) ↔ ((φ ¬ φ) (ψ ¬ φ)))
4 pm3.24 626 . . . . . 6 ¬ (φ ¬ φ)
54biorfi 664 . . . . 5 ((ψ ¬ φ) ↔ ((ψ ¬ φ) (φ ¬ φ)))
6 andir 731 . . . . 5 (((φ ψ) ¬ φ) ↔ ((φ ¬ φ) (ψ ¬ φ)))
73, 5, 63bitr4ri 202 . . . 4 (((φ ψ) ¬ φ) ↔ (ψ ¬ φ))
8 pm5.61 707 . . . 4 (((φ ψ) ¬ ψ) ↔ (φ ¬ ψ))
97, 8orbi12i 680 . . 3 ((((φ ψ) ¬ φ) ((φ ψ) ¬ ψ)) ↔ ((ψ ¬ φ) (φ ¬ ψ)))
101, 2, 93bitri 195 . 2 ((φψ) ↔ ((ψ ¬ φ) (φ ¬ ψ)))
11 orcom 646 . 2 (((ψ ¬ φ) (φ ¬ ψ)) ↔ ((φ ¬ ψ) (ψ ¬ φ)))
12 ancom 253 . . 3 ((ψ ¬ φ) ↔ (¬ φ ψ))
1312orbi2i 678 . 2 (((φ ¬ ψ) (ψ ¬ φ)) ↔ ((φ ¬ ψ) φ ψ)))
1410, 11, 133bitri 195 1 ((φψ) ↔ ((φ ¬ ψ) φ ψ)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   ∧ wa 97   ↔ wb 98   ∨ wo 628   ⊻ wxo 1265 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629 This theorem depends on definitions:  df-bi 110  df-xor 1266 This theorem is referenced by:  xordc  1280  symdifxor  3197
 Copyright terms: Public domain W3C validator