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