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

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

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