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

Definition df-xor 1416
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 1458) and the constant false F. (df-fal 1461), we will be able to prove these truth table values:  ( ( T.  \/_ T.  ) 
<-> F.  ) (truxortru 1502), 
( ( T.  \/_ F.  )  <-> T.  ) (truxorfal 1503),  ( ( F.  \/_ T.  )  <-> T.  ) (falxortru 1504), and  ( ( F.  \/_ F.  )  <-> F.  ) (falxorfal 1506). Contrast with  /\ (df-an 377), 
\/ (df-or 376), 
-> (wi 4), and  -/\ (df-nan 1395) . (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 1415 . 2  wff  ( ph  \/_ 
ps )
41, 2wb 189 . . 3  wff  ( ph  <->  ps )
54wn 3 . 2  wff  -.  ( ph 
<->  ps )
63, 5wb 189 1  wff  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1417  xorcom  1418  xorass  1419  xorassOLD  1420  excxor  1421  xor2  1422  xorneg2  1426  xorneg1OLD  1428  xorbi12i  1431  xorbi12d  1432  anxordi  1433  xorexmid  1434  truxortru  1502  truxorfal  1503  falxortruOLD  1505  falxorfal  1506  hadbi  1512  sadadd2lem2  14479  f1omvdco3  17145  tsxo3  32427  tsxo4  32428  ifpxorxorb  36201  axorbtnotaiffb  38625  axorbciffatcxorb  38627  aisbnaxb  38633  abnotbtaxb  38638  abnotataxb  38639
  Copyright terms: Public domain W3C validator