Metamath Proof Explorer


Theorem necon4abid

Description: Contrapositive law deduction for inequality. (Contributed by NM, 11-Jan-2008) (Proof shortened by Wolf Lammen, 24-Nov-2019)

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

Proof

Step Hyp Ref Expression
1 necon4abid.1 φAB¬ψ
2 notnotb ψ¬¬ψ
3 1 necon1bbid φ¬¬ψA=B
4 2 3 bitr2id φA=Bψ