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

Metamath Proof Explorer

Theorem impbii

Description: Infer an equivalence from an implication and its converse. Inference associated with impbi . (Contributed by NM, 29-Dec-1992)

Ref Expression
Hypotheses impbii.1 ⊢ φ → ψ
impbii.2 ⊢ ψ → φ
Assertion impbii ⊢ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 impbii.1 ⊢ φ → ψ
2 impbii.2 ⊢ ψ → φ
3 impbi ⊢ φ → ψ → ψ → φ → φ ↔ ψ
4 1 2 3 mp2 ⊢ φ ↔ ψ