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 1401) and the constant false F. (df-fal 1404), we will be able to prove these truth table values:  ( ( T.  \/_ T.  ) 
<-> F.  ) (truxortru 1444), 
( ( T.  \/_ F.  )  <-> T.  ) (truxorfal 1445),  ( ( F.  \/_ T.  )  <-> T.  ) (falxortru 1446), and  ( ( F.  \/_ F.  )  <-> F.  ) (falxorfal 1447). Contrast with  /\ (df-an 369), 
\/ (df-or 368), 
-> (wi 4), and  -/\ (df-nan 1342) . (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  xorassOLD  1367  excxor  1368  xor2  1369  xorneg2  1373  xorneg1OLD  1375  xorbi12i  1378  xorbi12d  1379  anxordi  1380  xorexmid  1381  truxortru  1444  truxorfal  1445  falxortru  1446  falxorfal  1447  hadbi  1457  had0  1475  sadadd2lem2  14184  f1omvdco3  16673  tsxo3  30786  tsxo4  30787  axorbtnotaiffb  32337  axorbciffatcxorb  32339  aisbnaxb  32345  abnotbtaxb  32350  abnotataxb  32351  ifpxorxorb  38147
  Copyright terms: Public domain W3C validator