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

Theorem xorexmid 1379
Description: Exclusive-or variant of the law of the excluded middle (exmid 415). 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 360 . 2
2 df-xor 1364 . 2
31, 2mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  \/_wxo 1363
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 185  df-xor 1364
  Copyright terms: Public domain W3C validator