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

Definition df-xor 1363
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 1384) and the constant false F. (df-fal 1387), we will be able to prove these truth table values:  ( ( T.  \/_ T.  ) 
<-> F.  ) (truxortru 1427), 
( ( T.  \/_ F.  )  <-> T.  ) (truxorfal 1428),  ( ( F.  \/_ T.  )  <-> T.  ) (falxortru 1429), and  ( ( F.  \/_ F.  )  <-> F.  ) (falxorfal 1430). Contrast with  /\ (df-an 371), 
\/ (df-or 370), 
-> (wi 4), and  -/\ (df-nan 1343) . (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 1362 . 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  1364  xorcom  1365  xorass  1366  excxor  1367  xor2  1368  xorneg1  1372  xorbi12i  1375  xorbi12d  1376  anxordi  1377  xorexmid  1378  truxortru  1427  truxorfal  1428  falxortru  1429  falxorfal  1430  hadbi  1440  had0  1456  sadadd2lem2  13974  f1omvdco3  16345  tsxo3  30518  tsxo4  30519  axorbtnotaiffb  31936  axorbciffatcxorb  31938  aisbnaxb  31944  abnotbtaxb  31949  abnotataxb  31950
  Copyright terms: Public domain W3C validator