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  mpto2OLD  1525  mtp-xorOLD  1527  sadadd2lem2  12657  f1omvdco3  27495  axorbtnotaiffb  27974  axorbciffatcxorb  27976  aisbnaxb  27982  abnotbtaxb  27987  abnotataxb  27988
  Copyright terms: Public domain W3C validator