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

Definition df-xor 1296
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 1310) and the constant false  F. (df-fal 1311), we will be able to prove these truth table values:  ( (  T.  \/_  T.  ) 
<->  F.  ) (truxortru 1348), 
( (  T.  \/_  F.  )  <->  T.  ) (truxorfal 1349),  ( (  F.  \/_  T.  )  <->  T.  ) (falxortru 1350), and  ( (  F.  \/_  F.  )  <->  F.  ) (falxorfal 1351). Contrast with  /\ (df-an 360), 
\/ (df-or 359), 
-> (wi 4), and  -/\ (df-nan 1288) . (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 1295 . 2  wff  ( ph \/_ ps )
41, 2wb 176 . . 3  wff  ( ph  <->  ps )
54wn 3 . 2  wff  -.  ( ph 
<->  ps )
63, 5wb 176 1  wff  ( (
ph \/_ ps )  <->  -.  ( ph 
<->  ps ) )
Colors of variables: wff set class
This definition is referenced by:  xnor  1297  xorcom  1298  xorass  1299  excxor  1300  xor2  1301  xorneg1  1302  xorbi12i  1305  xorbi12d  1306  truxortru  1348  truxorfal  1349  falxortru  1350  falxorfal  1351  hadbi  1377  had0  1393  mpto2  1524  mtp-xor  1525  sadadd2lem2  12641  f1omvdco3  27392  axorbtnotaiffb  27871  axorbciffatcxorb  27873  aisbnaxb  27879  abnotbtaxb  27884  abnotataxb  27885
  Copyright terms: Public domain W3C validator