This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )