Theorem syl2anc 19

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

Hypotheses

Ref	Expression
syl2anc.1	|- R |= S
syl2anc.2	|- R |= T
syl2anc.3	|- (S, T) |= A

Assertion

Ref	Expression
syl2anc	|- R |= A

Proof of Theorem syl2anc

Step	Hyp	Ref	Expression
1		syl2anc.1	. . 3 |- R |= S
2		syl2anc.2	. . 3 |- R |= T
3	1, 2	jca 18	. 2 |- R |= (S, T)
4		syl2anc.3	. 2 |- (S, T) |= A
5	3, 4	syl 16	1 |- R |= A

Syntax hints:  kct 10   |= wffMMJ2 11

This theorem was proved from axioms:  ax-syl 15  ax-jca 17

This theorem is referenced by:  mpdan  35  syldan  36  trul  39  eqcomx  52  ancoms  54  sylan  59  an32s  60  anassrs  62  ceq12  88  hbxfr  108