Metamath Proof Explorer

Theorem syl11

Description: A syllogism inference. Commuted form of an instance of syl . (Contributed by BJ, 25-Oct-2021)

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


Step Hyp Ref Expression
1 syl11.1 φ ψ χ
2 syl11.2 θ φ
3 2 1 syl θ ψ χ
4 3 com12 ψ θ χ