Metamath Proof Explorer


Theorem biimpri

Description: Infer a converse implication from a logical equivalence. Inference associated with biimpr . (Contributed by NM, 29-Dec-1992) (Proof shortened by Wolf Lammen, 16-Sep-2013)

Ref Expression
Hypothesis biimpri.1 φ ψ
Assertion biimpri ψ φ

Proof

Step Hyp Ref Expression
1 biimpri.1 φ ψ
2 1 bicomi ψ φ
3 2 biimpi ψ φ