Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 xor2 ( ( 𝜑𝜓 ) ↔ ( ( 𝜑𝜓 ) ∧ ¬ ( 𝜑𝜓 ) ) )
2 df-or ( ( 𝜑𝜓 ) ↔ ( ¬ 𝜑𝜓 ) )
3 imnan ( ( 𝜑 → ¬ 𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
4 3 bicomi ( ¬ ( 𝜑𝜓 ) ↔ ( 𝜑 → ¬ 𝜓 ) )
5 2 4 anbi12i ( ( ( 𝜑𝜓 ) ∧ ¬ ( 𝜑𝜓 ) ) ↔ ( ( ¬ 𝜑𝜓 ) ∧ ( 𝜑 → ¬ 𝜓 ) ) )
6 df-an ( ( ( ¬ 𝜑𝜓 ) ∧ ( 𝜑 → ¬ 𝜓 ) ) ↔ ¬ ( ( ¬ 𝜑𝜓 ) → ¬ ( 𝜑 → ¬ 𝜓 ) ) )
7 1 5 6 3bitri ( ( 𝜑𝜓 ) ↔ ¬ ( ( ¬ 𝜑𝜓 ) → ¬ ( 𝜑 → ¬ 𝜓 ) ) )