Theorem xor

Description: Two ways to express exclusive disjunction ( df-xor ). Theorem *5.22 of WhiteheadRussell p. 124. (Contributed by NM, 3-Jan-2005) (Proof shortened by Wolf Lammen, 22-Jan-2013)

	Ref	Expression
Assertion	xor	|- ( -. ( ph <-> ps ) <-> ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		iman	|- ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
2		iman	|- ( ( ps -> ph ) <-> -. ( ps /\ -. ph ) )
3	1 2	anbi12i	|- ( ( ( ph -> ps ) /\ ( ps -> ph ) ) <-> ( -. ( ph /\ -. ps ) /\ -. ( ps /\ -. ph ) ) )
4		dfbi2	|- ( ( ph <-> ps ) <-> ( ( ph -> ps ) /\ ( ps -> ph ) ) )
5		ioran	|- ( -. ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) <-> ( -. ( ph /\ -. ps ) /\ -. ( ps /\ -. ph ) ) )
6	3 4 5	3bitr4ri	|- ( -. ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) <-> ( ph <-> ps ) )
7	6	con1bii	|- ( -. ( ph <-> ps ) <-> ( ( ph /\ -. ps ) \/ ( ps /\ -. ph ) ) )