Definition df-xor 1364

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 1398) and the constant false (df-fal 1401), we will be able to prove these truth table values: (truxortru 1441), (truxorfal 1442), (falxortru 1443), and (falxorfal 1444). Contrast with /\ (df-an 371), \/ (df-or 370), -> (wi 4), and -/\ (df-nan 1344) . (Contributed by FL, 22-Nov-2010.)

Assertion

Ref	Expression
df-xor

Detailed syntax breakdown of Definition df-xor

Step	Hyp	Ref	Expression
1		wph	. . 3
2		wps	. . 3
3	1, 2	wxo 1363	. 2
4	1, 2	wb 184	. . 3
5	4	wn 3	. 2
6	3, 5	wb 184	1

This definition is referenced by:  xnor  1365  xorcom  1366  xorass  1367  excxor  1368  xor2  1369  xorneg1  1373  xorbi12i  1376  xorbi12d  1377  anxordi  1378  xorexmid  1379  truxortru  1441  truxorfal  1442  falxortru  1443  falxorfal  1444  hadbi  1454  had0  1471  sadadd2lem2  14100  f1omvdco3  16474  tsxo3  30546  tsxo4  30547  axorbtnotaiffb  32098  axorbciffatcxorb  32100  aisbnaxb  32106  abnotbtaxb  32111  abnotataxb  32112  bj-ifxorxorb  37733