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

Definition df-xor 1361
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 1382) and the constant false F. (df-fal 1385), we will be able to prove these truth table values:  ( ( T.  \/_ T.  ) 
<-> F.  ) (truxortru 1425), 
( ( T.  \/_ F.  )  <-> T.  ) (truxorfal 1426),  ( ( F.  \/_ T.  )  <-> T.  ) (falxortru 1427), and  ( ( F.  \/_ F.  )  <-> F.  ) (falxorfal 1428). Contrast with  /\ (df-an 371), 
\/ (df-or 370), 
-> (wi 4), and  -/\ (df-nan 1344) . (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 1360 . 2  wff  ( ph  \/_ 
ps )
41, 2wb 184 . . 3  wff  ( ph  <->  ps )
54wn 3 . 2  wff  -.  ( ph 
<->  ps )
63, 5wb 184 1  wff  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1362  xorcom  1363  xorass  1364  excxor  1365  xor2  1366  xorneg1  1370  xorbi12i  1373  xorbi12d  1374  anxordi  1375  xorexmid  1376  truxortru  1425  truxorfal  1426  falxortru  1427  falxorfal  1428  hadbi  1438  had0  1455  sadadd2lem2  13955  f1omvdco3  16270  tsxo3  30150  tsxo4  30151  axorbtnotaiffb  31565  axorbciffatcxorb  31567  aisbnaxb  31573  abnotbtaxb  31578  abnotataxb  31579
  Copyright terms: Public domain W3C validator