Theorem jca 18

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

Hypotheses

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

Assertion

Ref	Expression
jca	⊢ R⊧(S, T)

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		ax-jca.1	. 2 ⊢ R⊧S
2		ax-jca.2	. 2 ⊢ R⊧T
3	1, 2	ax-jca 17	1 ⊢ R⊧(S, T)

Syntax hints:  kct 10  ⊧wffMMJ2 11

This theorem was proved from axioms:  ax-jca 17

This theorem is referenced by:  syl2anc  19  ct1  57  ct2  58  dfan2  154  ex  158