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

Metamath Proof Explorer

Theorem sylsyld

Description: A double syllogism inference. (Contributed by Alan Sare, 20-Apr-2011)

Ref Expression
Hypotheses sylsyld.1 ⊢ φ → ψ
sylsyld.2 ⊢ φ → χ → θ
sylsyld.3 ⊢ ψ → θ → τ
Assertion sylsyld ⊢ φ → χ → τ

Proof

Step Hyp Ref Expression
1 sylsyld.1 ⊢ φ → ψ
2 sylsyld.2 ⊢ φ → χ → θ
3 sylsyld.3 ⊢ ψ → θ → τ
4 1 3 syl ⊢ φ → θ → τ
5 2 4 syld ⊢ φ → χ → τ