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

Theorem xor3 358
Description: Two ways to express "exclusive or." (Contributed by NM, 1-Jan-2006.)
Assertion
Ref Expression
xor3  |-  ( -.  ( ph  <->  ps )  <->  (
ph 
<->  -.  ps ) )

Proof of Theorem xor3
StepHypRef Expression
1 pm5.18 357 . . 3  |-  ( (
ph 
<->  ps )  <->  -.  ( ph 
<->  -.  ps ) )
21con2bii 333 . 2  |-  ( (
ph 
<->  -.  ps )  <->  -.  ( ph 
<->  ps ) )
32bicomi 205 1  |-  ( -.  ( ph  <->  ps )  <->  (
ph 
<->  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 187
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
This theorem is referenced by:  nbbn  359  pm5.15  897  nbi2  900  xorass  1404  hadnot  1500  nabbi  2756  nabbiOLD  2757  symdifass  3699  notzfaus  4591  nmogtmnf  26282  nmopgtmnf  27382  limsucncmpi  30916  aiffnbandciffatnotciffb  37924  axorbciffatcxorb  37925  abnotbtaxb  37936
  Copyright terms: Public domain W3C validator