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