Metamath Proof Explorer


Theorem cdeqnot

Description: Distribute conditional equality over negation. (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypothesis cdeqnot.1 CondEq ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion cdeqnot CondEq ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 cdeqnot.1 CondEq ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 1 cdeqri ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
3 2 notbid ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
4 3 cdeqi CondEq ( 𝑥 = 𝑦 → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )