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	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2	0 1	wxo	⊢ ( 𝜑 ⊻ 𝜓 )
3	0 1	wb	⊢ ( 𝜑 ↔ 𝜓 )
4	3	wn	⊢ ¬ ( 𝜑 ↔ 𝜓 )
5	2 4	wb	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )