Theorem dfxor4

Description: Express exclusive-or in terms of implication and negation. Statement in Frege1879 p. 12. (Contributed by RP, 14-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		xor2	|- ( ( ph \/_ ps ) <-> ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) )
2		df-or	|- ( ( ph \/ ps ) <-> ( -. ph -> ps ) )
3		imnan	|- ( ( ph -> -. ps ) <-> -. ( ph /\ ps ) )
4	3	bicomi	|- ( -. ( ph /\ ps ) <-> ( ph -> -. ps ) )
5	2 4	anbi12i	|- ( ( ( ph \/ ps ) /\ -. ( ph /\ ps ) ) <-> ( ( -. ph -> ps ) /\ ( ph -> -. ps ) ) )
6		df-an	|- ( ( ( -. ph -> ps ) /\ ( ph -> -. ps ) ) <-> -. ( ( -. ph -> ps ) -> -. ( ph -> -. ps ) ) )
7	1 5 6	3bitri	|- ( ( ph \/_ ps ) <-> -. ( ( -. ph -> ps ) -> -. ( ph -> -. ps ) ) )