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	|- ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2	0 1	wxo	|- ( ph \/_ ps )
3	0 1	wb	|- ( ph <-> ps )
4	3	wn	|- -. ( ph <-> ps )
5	2 4	wb	|- ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )