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

Theorem anxordi 1378
Description: Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 895 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 895 . 2
2 df-xor 1364 . . 3
32anbi2i 694 . 2
4 df-xor 1364 . 2
51, 3, 43bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  /\wa 369  \/_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-an 371  df-xor 1364
  Copyright terms: Public domain W3C validator