Definition df-xor 1416

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 1458) and the constant false F. (df-fal 1461), we will be able to prove these truth table values: ( ( T. \/_ T. ) <-> F. ) (truxortru 1502), ( ( T. \/_ F. ) <-> T. ) (truxorfal 1503), ( ( F. \/_ T. ) <-> T. ) (falxortru 1504), and ( ( F. \/_ F. ) <-> F. ) (falxorfal 1506). Contrast with /\ (df-an 377), \/ (df-or 376), -> (wi 4), and -/\ (df-nan 1395) . (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 1415	. 2 wff ( ph \/_ ps )
4	1, 2	wb 189	. . 3 wff ( ph <-> ps )
5	4	wn 3	. 2 wff -. ( ph <-> ps )
6	3, 5	wb 189	1 wff ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )

This definition is referenced by:  xnor  1417  xorcom  1418  xorass  1419  xorassOLD  1420  excxor  1421  xor2  1422  xorneg2  1426  xorneg1OLD  1428  xorbi12i  1431  xorbi12d  1432  anxordi  1433  xorexmid  1434  truxortru  1502  truxorfal  1503  falxortruOLD  1505  falxorfal  1506  hadbi  1512  sadadd2lem2  14479  f1omvdco3  17145  tsxo3  32427  tsxo4  32428  ifpxorxorb  36201  axorbtnotaiffb  38625  axorbciffatcxorb  38627  aisbnaxb  38633  abnotbtaxb  38638  abnotataxb  38639