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

Definition df-xor 1315
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 1329) and the constant false  F. (df-fal 1330), we will be able to prove these truth table values:  ( (  T.  \/_  T.  ) 
<->  F.  ) (truxortru 1368), 
( (  T.  \/_  F.  )  <->  T.  ) (truxorfal 1369),  ( (  F.  \/_  T.  )  <->  T.  ) (falxortru 1370), and  ( (  F.  \/_  F.  )  <->  F.  ) (falxorfal 1371). Contrast with  /\ (df-an 362), 
\/ (df-or 361), 
-> (wi 4), and  -/\ (df-nan 1298) . (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 1314 . 2  wff  ( ph  \/_ 
ps )
41, 2wb 178 . . 3  wff  ( ph  <->  ps )
54wn 3 . 2  wff  -.  ( ph 
<->  ps )
63, 5wb 178 1  wff  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
Colors of variables: wff set class
This definition is referenced by:  xnor  1316  xorcom  1317  xorass  1318  excxor  1319  xor2  1320  xorneg1  1321  xorbi12i  1324  xorbi12d  1325  truxortru  1368  truxorfal  1369  falxortru  1370  falxorfal  1371  hadbi  1397  had0  1413  mpto2  1544  mpto2OLD  1545  mtp-xorOLD  1547  sadadd2lem2  12963  f1omvdco3  27370  axorbtnotaiffb  27848  axorbciffatcxorb  27850  aisbnaxb  27856  abnotbtaxb  27861  abnotataxb  27862
  Copyright terms: Public domain W3C validator