Theorem dfxor5 36213

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

Assertion

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

Proof of Theorem dfxor5

Step	Hyp	Ref	Expression
1		dfxor4 36212	. 2 |- ( ( ph \/_ ps ) <-> -. ( ( -. ph -> ps ) -> -. ( ph -> -. ps ) ) )
2		con2b 335	. 2 |- ( ( ( -. ph -> ps ) -> -. ( ph -> -. ps ) ) <-> ( ( ph -> -. ps ) -> -. ( -. ph -> ps ) ) )
3	1, 2	xchbinx 311	1 |- ( ( ph \/_ ps ) <-> -. ( ( ph -> -. ps ) -> -. ( -. ph -> ps ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   \/_ wxo 1400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-xor 1401

This theorem is referenced by: (None)