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 T. (df-tru 1373) and the constant false F. (df-fal 1376), we will be able to prove these truth table values: ( ( T. \/_ T. ) <-> F. ) (truxortru 1416), ( ( T. \/_ F. ) <-> T. ) (truxorfal 1417), ( ( F. \/_ T. ) <-> T. ) (falxortru 1418), and ( ( F. \/_ F. ) <-> F. ) (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	|- ( ( 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 1351	. 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  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  13757  f1omvdco3  16066  tsxo3  29091  tsxo4  29092  axorbtnotaiffb  30058  axorbciffatcxorb  30060  aisbnaxb  30066  abnotbtaxb  30071  abnotataxb  30072