Definition df-xor 1363

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 1401) and the constant false F. (df-fal 1404), we will be able to prove these truth table values: ( ( T. \/_ T. ) <-> F. ) (truxortru 1444), ( ( T. \/_ F. ) <-> T. ) (truxorfal 1445), ( ( F. \/_ T. ) <-> T. ) (falxortru 1446), and ( ( F. \/_ F. ) <-> F. ) (falxorfal 1447). Contrast with /\ (df-an 369), \/ (df-or 368), -> (wi 4), and -/\ (df-nan 1342) . (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 1362	. 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  1364  xorcom  1365  xorass  1366  xorassOLD  1367  excxor  1368  xor2  1369  xorneg2  1373  xorneg1OLD  1375  xorbi12i  1378  xorbi12d  1379  anxordi  1380  xorexmid  1381  truxortru  1444  truxorfal  1445  falxortru  1446  falxorfal  1447  hadbi  1457  had0  1475  sadadd2lem2  14184  f1omvdco3  16673  tsxo3  30786  tsxo4  30787  axorbtnotaiffb  32337  axorbciffatcxorb  32339  aisbnaxb  32345  abnotbtaxb  32350  abnotataxb  32351  ifpxorxorb  38147