 Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  anxordi Structured version   Visualization version   GIF version

Theorem anxordi 1471
 Description: Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 935 does not necessarily hold, in part because the usual definition of xor is subtly different in intuitionistic logic. (Contributed by David A. Wheeler, 7-Oct-2018.)
Assertion
Ref Expression
anxordi ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ⊻ (𝜑𝜒)))

Proof of Theorem anxordi
StepHypRef Expression
1 xordi 935 . 2 ((𝜑 ∧ ¬ (𝜓𝜒)) ↔ ¬ ((𝜑𝜓) ↔ (𝜑𝜒)))
2 df-xor 1457 . . 3 ((𝜓𝜒) ↔ ¬ (𝜓𝜒))
32anbi2i 726 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜑 ∧ ¬ (𝜓𝜒)))
4 df-xor 1457 . 2 (((𝜑𝜓) ⊻ (𝜑𝜒)) ↔ ¬ ((𝜑𝜓) ↔ (𝜑𝜒)))
51, 3, 43bitr4i 291 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ⊻ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195   ∧ wa 383   ⊻ wxo 1456 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 196  df-an 385  df-xor 1457 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator