Metamath Proof Explorer


Theorem xorneg

Description: The connector \/_ is unchanged under negation of both arguments. (Contributed by Mario Carneiro, 4-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 xorneg1 ( ( ¬ 𝜑 ⊻ ¬ 𝜓 ) ↔ ¬ ( 𝜑 ⊻ ¬ 𝜓 ) )
2 xorneg2 ( ( 𝜑 ⊻ ¬ 𝜓 ) ↔ ¬ ( 𝜑𝜓 ) )
3 2 con2bii ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑 ⊻ ¬ 𝜓 ) )
4 1 3 bitr4i ( ( ¬ 𝜑 ⊻ ¬ 𝜓 ) ↔ ( 𝜑𝜓 ) )