Metamath Proof Explorer

Theorem sylbi

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993)

Ref Expression
Hypotheses sylbi.1 φ ψ
sylbi.2 ψ χ
Assertion sylbi φ χ


Step Hyp Ref Expression
1 sylbi.1 φ ψ
2 sylbi.2 ψ χ
3 1 biimpi φ ψ
4 3 2 syl φ χ