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

Definition df-xor 1352
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 (df-tru 1373) and the constant false (df-fal 1376), we will be able to prove these truth table values: (truxortru 1416), (truxorfal 1417), (falxortru 1418), and (falxorfal 1419). Contrast with /\ (df-an 371), \/ (df-or 370), -> (wi 4), and -/\ (df-nan 1335) . (Contributed by FL, 22-Nov-2010.)
Assertion
Ref Expression
df-xor

Detailed syntax breakdown of Definition df-xor
StepHypRef Expression
1 wph . . 3
2 wps . . 3
31, 2wxo 1351 . 2
41, 2wb 184 . . 3
54wn 3 . 2
63, 5wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  xnor  1353  xorcom  1354  xorass  1355  excxor  1356  xor2  1357  xorneg1  1361  xorbi12i  1364  xorbi12d  1365  anxordi  1366  xorexmid  1367  truxortru  1416  truxorfal  1417  falxortru  1418  falxorfal  1419  hadbi  1429  had0  1446  sadadd2lem2  13804  f1omvdco3  16114  tsxo3  29410  tsxo4  29411  axorbtnotaiffb  30794  axorbciffatcxorb  30796  aisbnaxb  30802  abnotbtaxb  30807  abnotataxb  30808
  Copyright terms: Public domain W3C validator