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

Theorem anxordi 1418
Description: Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 903 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  |-  ( (
ph  /\  ( ps  \/_ 
ch ) )  <->  ( ( ph  /\  ps )  \/_  ( ph  /\  ch )
) )

Proof of Theorem anxordi
StepHypRef Expression
1 xordi 903 . 2  |-  ( (
ph  /\  -.  ( ps 
<->  ch ) )  <->  -.  (
( ph  /\  ps )  <->  (
ph  /\  ch )
) )
2 df-xor 1401 . . 3  |-  ( ( ps  \/_  ch )  <->  -.  ( ps  <->  ch )
)
32anbi2i 698 . 2  |-  ( (
ph  /\  ( ps  \/_ 
ch ) )  <->  ( ph  /\ 
-.  ( ps  <->  ch )
) )
4 df-xor 1401 . 2  |-  ( ( ( ph  /\  ps )  \/_  ( ph  /\  ch ) )  <->  -.  (
( ph  /\  ps )  <->  (
ph  /\  ch )
) )
51, 3, 43bitr4i 280 1  |-  ( (
ph  /\  ( ps  \/_ 
ch ) )  <->  ( ( ph  /\  ps )  \/_  ( ph  /\  ch )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187    /\ wa 370    \/_ wxo 1400
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 188  df-an 372  df-xor 1401
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator