Metamath Proof Explorer

Theorem syl2imc

Description: A commuted version of syl2im . Implication-only version of syl2anr . (Contributed by BJ, 20-Oct-2021)

Ref Expression
Hypotheses syl2im.1 φ ψ
syl2im.2 χ θ
syl2im.3 ψ θ τ
Assertion syl2imc χ φ τ


Step Hyp Ref Expression
1 syl2im.1 φ ψ
2 syl2im.2 χ θ
3 syl2im.3 ψ θ τ
4 1 2 3 syl2im φ χ τ
5 4 com12 χ φ τ