Metamath Proof Explorer


Theorem syl3an

Description: A triple syllogism inference. (Contributed by NM, 13-May-2004)

Ref Expression
Hypotheses syl3an.1 φψ
syl3an.2 χθ
syl3an.3 τη
syl3an.4 ψθηζ
Assertion syl3an φχτζ

Proof

Step Hyp Ref Expression
1 syl3an.1 φψ
2 syl3an.2 χθ
3 syl3an.3 τη
4 syl3an.4 ψθηζ
5 1 2 3 3anim123i φχτψθη
6 5 4 syl φχτζ