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

Theorem xor3 384
Description: Two ways to express "exclusive or". (Contributed by NM, 1-Jan-2006.)
Assertion
Ref Expression
xor3 (¬ (𝜑𝜓) ↔ (𝜑 ↔ ¬ 𝜓))

Proof of Theorem xor3
StepHypRef Expression
1 pm5.18 383 . . 3 ((𝜑𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓))
21con2bii 359 . 2 ((𝜑 ↔ ¬ 𝜓) ↔ ¬ (𝜑𝜓))
32bicomi 225 1 (¬ (𝜑𝜓) ↔ (𝜑 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207
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 208
This theorem is referenced by:  nbbn  385  pm5.15  1006  nbi2  1009  xorass  1499  hadnot  1594  nabbi  3118  notzfausOLD  5254  nmogtmnf  28474  nmopgtmnf  29572  limsucncmpi  33690  aiffnbandciffatnotciffb  43017  axorbciffatcxorb  43018  abnotbtaxb  43028  afv2orxorb  43304  line2ylem  44666  line2xlem  44668
  Copyright terms: Public domain W3C validator