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 1384) and the constant false F. (df-fal 1387), we will be able to prove these truth table values: ( ( T. \/_ T. ) <-> F. ) (truxortru 1427), ( ( T. \/_ F. ) <-> T. ) (truxorfal 1428), ( ( F. \/_ T. ) <-> T. ) (falxortru 1429), and ( ( F. \/_ F. ) <-> F. ) (falxorfal 1430). Contrast with /\ (df-an 371), \/ (df-or 370), -> (wi 4), and -/\ (df-nan 1343) . (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  excxor  1367  xor2  1368  xorneg1  1372  xorbi12i  1375  xorbi12d  1376  anxordi  1377  xorexmid  1378  truxortru  1427  truxorfal  1428  falxortru  1429  falxorfal  1430  hadbi  1440  had0  1456  sadadd2lem2  13974  f1omvdco3  16345  tsxo3  30518  tsxo4  30519  axorbtnotaiffb  31936  axorbciffatcxorb  31938  aisbnaxb  31944  abnotbtaxb  31949  abnotataxb  31950