Metamath Proof Explorer

Theorem nanorxor

Description: 'nand' is equivalent to the equivalence of inclusive and exclusive or. (Contributed by Steve Rodriguez, 28-Feb-2020)

Ref Expression
Assertion nanorxor ⊢ φ ⊼ ψ ↔ φ ∨ ψ ↔ φ ⊻ ψ

Proof

Step Hyp Ref Expression
1 df-nan ⊢ φ ⊼ ψ ↔ ¬ φ ∧ ψ
2 xor2 ⊢ φ ⊻ ψ ↔ φ ∨ ψ ∧ ¬ φ ∧ ψ
3 2 rbaibr ⊢ ¬ φ ∧ ψ → φ ∨ ψ ↔ φ ⊻ ψ
4 2 bibi2i ⊢ φ ∨ ψ ↔ φ ⊻ ψ ↔ φ ∨ ψ ↔ φ ∨ ψ ∧ ¬ φ ∧ ψ
5 pm4.71 ⊢ φ ∨ ψ → ¬ φ ∧ ψ ↔ φ ∨ ψ ↔ φ ∨ ψ ∧ ¬ φ ∧ ψ
6 simpl ⊢ φ ∧ ψ → φ
7 6 orcd ⊢ φ ∧ ψ → φ ∨ ψ
8 7 con3i ⊢ ¬ φ ∨ ψ → ¬ φ ∧ ψ
9 id ⊢ ¬ φ ∧ ψ → ¬ φ ∧ ψ
10 8 9 ja ⊢ φ ∨ ψ → ¬ φ ∧ ψ → ¬ φ ∧ ψ
11 5 10 sylbir ⊢ φ ∨ ψ ↔ φ ∨ ψ ∧ ¬ φ ∧ ψ → ¬ φ ∧ ψ
12 4 11 sylbi ⊢ φ ∨ ψ ↔ φ ⊻ ψ → ¬ φ ∧ ψ
13 3 12 impbii ⊢ ¬ φ ∧ ψ ↔ φ ∨ ψ ↔ φ ⊻ ψ
14 1 13 bitri ⊢ φ ⊼ ψ ↔ φ ∨ ψ ↔ φ ⊻ ψ