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