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

Theorem anxordi 1527
Description: Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 1016 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 1016 . 2 ((𝜑 ∧ ¬ (𝜓𝜒)) ↔ ¬ ((𝜑𝜓) ↔ (𝜑𝜒)))
2 df-xor 1511 . . 3 ((𝜓𝜒) ↔ ¬ (𝜓𝜒))
32anbi2i 624 . 2 ((𝜑 ∧ (𝜓𝜒)) ↔ (𝜑 ∧ ¬ (𝜓𝜒)))
4 df-xor 1511 . 2 (((𝜑𝜓) ⊻ (𝜑𝜒)) ↔ ¬ ((𝜑𝜓) ↔ (𝜑𝜒)))
51, 3, 43bitr4i 303 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ⊻ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397  wxo 1510
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 206  df-an 398  df-xor 1511
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator