Metamath Proof Explorer


Theorem necon2bi

Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007)

Ref Expression
Hypothesis necon2bi.1 φ A B
Assertion necon2bi A = B ¬ φ

Proof

Step Hyp Ref Expression
1 necon2bi.1 φ A B
2 1 neneqd φ ¬ A = B
3 2 con2i A = B ¬ φ