Metamath Proof Explorer


Theorem xorneg2

Description: The connector \/_ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016) (Proof shortened by Wolf Lammen, 27-Jun-2020)

Ref Expression
Assertion xorneg2 ( ( 𝜑 ⊻ ¬ 𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )

Proof

Step Hyp Ref Expression
1 df-xor ( ( 𝜑 ⊻ ¬ 𝜓 ) ↔ ¬ ( 𝜑 ↔ ¬ 𝜓 ) )
2 pm5.18 ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑 ↔ ¬ 𝜓 ) )
3 xnor ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
4 1 2 3 3bitr2i ( ( 𝜑 ⊻ ¬ 𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )