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