Metamath Proof Explorer


Theorem necon4bd

Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 23-Nov-2019)

Ref Expression
Hypothesis necon4bd.1 φ ¬ ψ A B
Assertion necon4bd φ A = B ψ

Proof

Step Hyp Ref Expression
1 necon4bd.1 φ ¬ ψ A B
2 1 necon2bd φ A = B ¬ ¬ ψ
3 notnotr ¬ ¬ ψ ψ
4 2 3 syl6 φ A = B ψ