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

Definition df-xor 1311
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 1325) and the constant false  F. (df-fal 1326), we will be able to prove these truth table values:  ( (  T.  \/_  T.  ) 
<->  F.  ) (truxortru 1364), 
( (  T.  \/_  F.  )  <->  T.  ) (truxorfal 1365),  ( (  F.  \/_  T.  )  <->  T.  ) (falxortru 1366), and  ( (  F.  \/_  F.  )  <->  F.  ) (falxorfal 1367). Contrast with  /\ (df-an 361), 
\/ (df-or 360), 
-> (wi 4), and  -/\ (df-nan 1294) . (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 1310 . 2  wff  ( ph  \/_ 
ps )
41, 2wb 177 . . 3  wff  ( ph  <->  ps )
54wn 3 . 2  wff  -.  ( ph 
<->  ps )
63, 5wb 177 1  wff  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
Colors of variables: wff set class
This definition is referenced by:  xnor  1312  xorcom  1313  xorass  1314  excxor  1315  xor2  1316  xorneg1  1317  xorbi12i  1320  xorbi12d  1321  truxortru  1364  truxorfal  1365  falxortru  1366  falxorfal  1367  hadbi  1393  had0  1409  mpto2  1540  mpto2OLD  1541  mtp-xorOLD  1543  sadadd2lem2  12925  f1omvdco3  27268  axorbtnotaiffb  27746  axorbciffatcxorb  27748  aisbnaxb  27754  abnotbtaxb  27759  abnotataxb  27760
  Copyright terms: Public domain W3C validator