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 ( ( 𝜑 ∧ ¬ ( 𝜓𝜒 ) ) ↔ ¬ ( ( 𝜑𝜓 ) ↔ ( 𝜑𝜒 ) ) )