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

Theorem xorexmid 1628
Description: Exclusive-or variant of the law of the excluded middle (exmid 880). This statement is ancient, going back to at least Stoic logic. This statement does not necessarily hold in intuitionistic logic. (Contributed by David A. Wheeler, 23-Feb-2019.)
Assertion
Ref Expression
xorexmid (𝜑 ⊻ ¬ 𝜑)

Proof of Theorem xorexmid
StepHypRef Expression
1 pm5.19 374 . 2 ¬ (𝜑 ↔ ¬ 𝜑)
2 df-xor 1613 . 2 ((𝜑 ⊻ ¬ 𝜑) ↔ ¬ (𝜑 ↔ ¬ 𝜑))
31, 2mpbir 221 1 (𝜑 ⊻ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wxo 1612
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 197  df-xor 1613
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator