Definition df-xor

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 ) and the constant false F. ( df-fal ), we will be able to prove these truth table values: ( ( T. \/_ T. ) <-> F. ) ( truxortru ), ( ( T. \/_ F. ) <-> T. ) ( truxorfal ), ( ( F. \/_ T. ) <-> T. ) ( falxortru ), and ( ( F. \/_ F. ) <-> F. ) ( falxorfal ). Contrast with /\ ( df-an ), \/ ( df-or ), -> ( wi ), and -/\ ( df-nan ). (Contributed by FL, 22-Nov-2010)

	Ref	Expression
Assertion	df-xor	$$⊢\left(\phi ⊻\psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \psi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2	0 1	wxo	$$wff\left(\phi ⊻\psi \right)$$
3	0 1	wb	$$wff\left(\phi \leftrightarrow \psi \right)$$
4	3	wn	$$wff\neg \left(\phi \leftrightarrow \psi \right)$$
5	2 4	wb	$$wff\left(\left(\phi ⊻\psi \right)\leftrightarrow \neg \left(\phi \leftrightarrow \psi \right)\right)$$