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

Definition df-xor 1314
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 1328) and the constant false  F. (df-fal 1329), we will be able to prove these truth table values:  ( (  T.  \/_  T.  ) 
<->  F.  ) (truxortru 1367), 
( (  T.  \/_  F.  )  <->  T.  ) (truxorfal 1368),  ( (  F.  \/_  T.  )  <->  T.  ) (falxortru 1369), and  ( (  F.  \/_  F.  )  <->  F.  ) (falxorfal 1370). Contrast with  /\ (df-an 361), 
\/ (df-or 360), 
-> (wi 4), and  -/\ (df-nan 1297) . (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 1313 . 2  wff  ( ph  \/_ 
ps )
41, 2wb 177 . . 3  wff  ( ph  <->  ps )
54wn 3 . 2  wff  -.  ( ph 
<->  ps )
63, 5wb 177 1  wff  ( (
ph  \/_  ps )  <->  -.  ( ph  <->  ps )
)
Colors of variables: wff set class
This definition is referenced by:  xnor  1315  xorcom  1316  xorass  1317  excxor  1318  xor2  1319  xorneg1  1320  xorbi12i  1323  xorbi12d  1324  truxortru  1367  truxorfal  1368  falxortru  1369  falxorfal  1370  hadbi  1396  had0  1412  mpto2  1543  mpto2OLD  1544  mtp-xorOLD  1546  sadadd2lem2  12962  f1omvdco3  27369  axorbtnotaiffb  27847  axorbciffatcxorb  27849  aisbnaxb  27855  abnotbtaxb  27860  abnotataxb  27861
  Copyright terms: Public domain W3C validator