Definition df-xor 1361

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 1382) and the constant false F. (df-fal 1385), we will be able to prove these truth table values: ( ( T. \/_ T. ) <-> F. ) (truxortru 1425), ( ( T. \/_ F. ) <-> T. ) (truxorfal 1426), ( ( F. \/_ T. ) <-> T. ) (falxortru 1427), and ( ( F. \/_ F. ) <-> F. ) (falxorfal 1428). 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	|- ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )

Detailed syntax breakdown of Definition df-xor

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3	1, 2	wxo 1360	. 2 wff ( ph \/_ ps )
4	1, 2	wb 184	. . 3 wff ( ph <-> ps )
5	4	wn 3	. 2 wff -. ( ph <-> ps )
6	3, 5	wb 184	1 wff ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )

This definition is referenced by:  xnor  1362  xorcom  1363  xorass  1364  excxor  1365  xor2  1366  xorneg1  1370  xorbi12i  1373  xorbi12d  1374  anxordi  1375  xorexmid  1376  truxortru  1425  truxorfal  1426  falxortru  1427  falxorfal  1428  hadbi  1438  had0  1455  sadadd2lem2  13955  f1omvdco3  16270  tsxo3  30150  tsxo4  30151  axorbtnotaiffb  31565  axorbciffatcxorb  31567  aisbnaxb  31573  abnotbtaxb  31578  abnotataxb  31579