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

Metamath Proof Explorer

Theorem syl6an

Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 syl6an.1 ⊢ φ → ψ
2 syl6an.2 ⊢ φ → χ → θ
3 syl6an.3 ⊢ ψ ∧ θ → τ
4 3 ex ⊢ ψ → θ → τ
5 1 2 4 sylsyld ⊢ φ → χ → τ