Definition df-xor 1351

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 1372) and the constant false F. (df-fal 1375), we will be able to prove these truth table values: ( ( T. \/_ T. ) <-> F. ) (truxortru 1415), ( ( T. \/_ F. ) <-> T. ) (truxorfal 1416), ( ( F. \/_ T. ) <-> T. ) (falxortru 1417), and ( ( F. \/_ F. ) <-> F. ) (falxorfal 1418). Contrast with /\ (df-an 371), \/ (df-or 370), -> (wi 4), and -/\ (df-nan 1334) . (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 1350	. 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  1352  xorcom  1353  xorass  1354  excxor  1355  xor2  1356  xorneg1  1360  xorbi12i  1363  xorbi12d  1364  anxordi  1365  xorexmid  1366  truxortru  1415  truxorfal  1416  falxortru  1417  falxorfal  1418  hadbi  1428  had0  1445  sadadd2lem2  13638  f1omvdco3  15946  tsxo3  28903  tsxo4  28904  axorbtnotaiffb  29870  axorbciffatcxorb  29872  aisbnaxb  29878  abnotbtaxb  29883  abnotataxb  29884