Theorem syl 16

Description: Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
ax-syl.1	⊢ R⊧S
ax-syl.2	⊢ S⊧T

Assertion

Ref	Expression
syl	⊢ R⊧T

Proof of Theorem syl

Step	Hyp	Ref	Expression
1		ax-syl.1	. 2 ⊢ R⊧S
2		ax-syl.2	. 2 ⊢ S⊧T
3	1, 2	ax-syl 15	1 ⊢ R⊧T

Syntax hints:  ⊧wffMMJ2 11

This theorem was proved from axioms:  ax-syl 15

This theorem is referenced by:  syl2anc  19  a1i  28  simpld  37  simprd  38  adantr  55  pm2.21  153  con3d  162  ecase  163  exlimdv2  166  cla4ev  169  19.8a  170  eta  178  exlimd  183  eximdv  185  exnal1  187  ac  197  exmid  199  notnot  200  ax3  205  ax7  209  ax9  212  ax11  214  axrep  220  axpow  221  axun  222