Metamath Proof Explorer

Theorem xordi

Description: Conjunction distributes over exclusive-or, using -. ( ph <-> ps ) to express exclusive-or. This is one way to interpret the distributive law of multiplication over addition in modulo 2 arithmetic. This is not necessarily true in intuitionistic logic, though anxordi does hold in it. (Contributed by NM, 3-Oct-2008)

Ref Expression
Assertion xordi ⊢ φ ∧ ¬ ψ ↔ χ ↔ ¬ φ ∧ ψ ↔ φ ∧ χ

Proof

Step Hyp Ref Expression
1 annim ⊢ φ ∧ ¬ ψ ↔ χ ↔ ¬ φ → ψ ↔ χ
2 pm5.32 ⊢ φ → ψ ↔ χ ↔ φ ∧ ψ ↔ φ ∧ χ
3 1 2 xchbinx ⊢ φ ∧ ¬ ψ ↔ χ ↔ ¬ φ ∧ ψ ↔ φ ∧ χ