Metamath Proof Explorer


Theorem syl3anb

Description: A triple syllogism inference. (Contributed by NM, 15-Oct-2005)

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

Proof

Step Hyp Ref Expression
1 syl3anb.1 φ ψ
2 syl3anb.2 χ θ
3 syl3anb.3 τ η
4 syl3anb.4 ψ θ η ζ
5 1 2 3 3anbi123i φ χ τ ψ θ η
6 5 4 sylbi φ χ τ ζ