Metamath Proof Explorer

Theorem biimpd

Description: Deduce an implication from a logical equivalence. Deduction associated with biimp and biimpi . (Contributed by NM, 11-Jan-1993)

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


Step Hyp Ref Expression
1 biimpd.1 φ ψ χ
2 biimp ψ χ ψ χ
3 1 2 syl φ ψ χ