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

Definition df-xor 1351
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 1372) and the constant false F. (df-fal 1375), we will be able to prove these truth table values:  ( ( T.  \/_ T.  ) 
<-> F.  ) (truxortru 1415), 
( ( T.  \/_ F.  )  <-> T.  ) (truxorfal 1416),  ( ( F.  \/_ T.  )  <-> T.  ) (falxortru 1417), and  ( ( F.  \/_ F.  )  <-> F.  ) (falxorfal 1418). Contrast with  /\ (df-an 371), 
\/ (df-or 370), 
-> (wi 4), and  -/\ (df-nan 1334) . (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 1350 . 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  1352  xorcom  1353  xorass  1354  excxor  1355  xor2  1356  xorneg1  1360  xorbi12i  1363  xorbi12d  1364  anxordi  1365  xorexmid  1366  truxortru  1415  truxorfal  1416  falxortru  1417  falxorfal  1418  hadbi  1428  had0  1445  sadadd2lem2  13638  f1omvdco3  15946  tsxo3  28903  tsxo4  28904  axorbtnotaiffb  29870  axorbciffatcxorb  29872  aisbnaxb  29878  abnotbtaxb  29883  abnotataxb  29884
  Copyright terms: Public domain W3C validator