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

Definition df-xor 1352
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 1373) and the constant false F. (df-fal 1376), we will be able to prove these truth table values:  ( ( T.  \/_ T.  ) 
<-> F.  ) (truxortru 1416), 
( ( T.  \/_ F.  )  <-> T.  ) (truxorfal 1417),  ( ( F.  \/_ T.  )  <-> T.  ) (falxortru 1418), and  ( ( F.  \/_ F.  )  <-> F.  ) (falxorfal 1419). Contrast with  /\ (df-an 371), 
\/ (df-or 370), 
-> (wi 4), and  -/\ (df-nan 1335) . (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 1351 . 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  1353  xorcom  1354  xorass  1355  excxor  1356  xor2  1357  xorneg1  1361  xorbi12i  1364  xorbi12d  1365  anxordi  1366  xorexmid  1367  truxortru  1416  truxorfal  1417  falxortru  1418  falxorfal  1419  hadbi  1429  had0  1446  sadadd2lem2  13757  f1omvdco3  16066  tsxo3  29091  tsxo4  29092  axorbtnotaiffb  30058  axorbciffatcxorb  30060  aisbnaxb  30066  abnotbtaxb  30071  abnotataxb  30072
  Copyright terms: Public domain W3C validator