This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ψ → θ → χ

Proof

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