Metamath Proof Explorer

Theorem syl5bi

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

Ref Expression
Hypotheses syl5bi.1 φ ψ
syl5bi.2 χ ψ θ
Assertion syl5bi χ φ θ


Step Hyp Ref Expression
1 syl5bi.1 φ ψ
2 syl5bi.2 χ ψ θ
3 1 biimpi φ ψ
4 3 2 syl5 χ φ θ