Definition df-xor 1401

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 1440) and the constant false F. (df-fal 1443), we will be able to prove these truth table values: ( ( T. \/_ T. ) <-> F. ) (truxortru 1484), ( ( T. \/_ F. ) <-> T. ) (truxorfal 1485), ( ( F. \/_ T. ) <-> T. ) (falxortru 1486), and ( ( F. \/_ F. ) <-> F. ) (falxorfal 1488). Contrast with /\ (df-an 372), \/ (df-or 371), -> (wi 4), and -/\ (df-nan 1380) . (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 1400	. 2 wff ( ph \/_ ps )
4	1, 2	wb 187	. . 3 wff ( ph <-> ps )
5	4	wn 3	. 2 wff -. ( ph <-> ps )
6	3, 5	wb 187	1 wff ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )

This definition is referenced by:  xnor  1402  xorcom  1403  xorass  1404  xorassOLD  1405  excxor  1406  xor2  1407  xorneg2  1411  xorneg1OLD  1413  xorbi12i  1416  xorbi12d  1417  anxordi  1418  xorexmid  1419  truxortru  1484  truxorfal  1485  falxortruOLD  1487  falxorfal  1488  hadbi  1494  sadadd2lem2  14360  f1omvdco3  17026  tsxo3  32282  tsxo4  32283  ifpxorxorb  36062  axorbtnotaiffb  38298  axorbciffatcxorb  38300  aisbnaxb  38306  abnotbtaxb  38311  abnotataxb  38312