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

Metamath Proof Explorer

Theorem syl56

Description: Combine syl5 and syl6 . (Contributed by NM, 14-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 syl56.1 ⊢ φ → ψ
2 syl56.2 ⊢ χ → ψ → θ
3 syl56.3 ⊢ θ → τ
4 2 3 syl6 ⊢ χ → ψ → τ
5 1 4 syl5 ⊢ χ → φ → τ