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

Definition df-xor 1401
Description: Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. After we define the constant true T. (df-tru 1440) and the constant false F. (df-fal 1443), we will be able to prove these truth table values:  ( ( T.  \/_ T.  ) 
<-> F.  ) (truxortru 1484), 
( ( T.  \/_ F.  )  <-> T.  ) (truxorfal 1485),  ( ( F.  \/_ T.  )  <-> T.  ) (falxortru 1486), and  ( ( F.  \/_ F.  )  <-> F.  ) (falxorfal 1488). Contrast with  /\ (df-an 372), 
\/ (df-or 371), 
-> (wi 4), and  -/\ (df-nan 1380) . (Contributed by FL, 22-Nov-2010.)
Assertion
Ref Expression
df-xor  |-  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)

Detailed syntax breakdown of Definition df-xor
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
31, 2wxo 1400 . 2  wff  ( ph  \/_ 
ps )
41, 2wb 187 . . 3  wff  ( ph  <->  ps )
54wn 3 . 2  wff  -.  ( ph 
<->  ps )
63, 5wb 187 1  wff  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1402  xorcom  1403  xorass  1404  xorassOLD  1405  excxor  1406  xor2  1407  xorneg2  1411  xorneg1OLD  1413  xorbi12i  1416  xorbi12d  1417  anxordi  1418  xorexmid  1419  truxortru  1484  truxorfal  1485  falxortruOLD  1487  falxorfal  1488  hadbi  1494  sadadd2lem2  14360  f1omvdco3  17026  tsxo3  32282  tsxo4  32283  ifpxorxorb  36062  axorbtnotaiffb  38298  axorbciffatcxorb  38300  aisbnaxb  38306  abnotbtaxb  38311  abnotataxb  38312
  Copyright terms: Public domain W3C validator