This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem necon2bbii

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

Ref Expression
Hypothesis necon2bbii.1 ⊢ φ ↔ A ≠ B
Assertion necon2bbii ⊢ A = B ↔ ¬ φ

Proof

Step Hyp Ref Expression
1 necon2bbii.1 ⊢ φ ↔ A ≠ B
2 1 bicomi ⊢ A ≠ B ↔ φ
3 2 necon1bbii ⊢ ¬ φ ↔ A = B
4 3 bicomi ⊢ A = B ↔ ¬ φ