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