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 φ ψ


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