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 φ χ τ