Metamath Proof Explorer


Theorem syl3anbrc

Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014)

Ref Expression
Hypotheses syl3anbrc.1 φψ
syl3anbrc.2 φχ
syl3anbrc.3 φθ
syl3anbrc.4 τψχθ
Assertion syl3anbrc φτ

Proof

Step Hyp Ref Expression
1 syl3anbrc.1 φψ
2 syl3anbrc.2 φχ
3 syl3anbrc.3 φθ
4 syl3anbrc.4 τψχθ
5 1 2 3 3jca φψχθ
6 5 4 sylibr φτ