Metamath Proof Explorer

Theorem biimprd

Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr and biimpri . (Contributed by NM, 11-Jan-1993) (Proof shortened by Wolf Lammen, 22-Sep-2013)

Ref Expression
Hypothesis biimprd.1 φ ψ χ
Assertion biimprd φ χ ψ


Step Hyp Ref Expression
1 biimprd.1 φ ψ χ
2 id χ χ
3 2 1 syl5ibr φ χ ψ