Theorem syl2anc 19

Description: Syllogism inference.

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  33  syldan  34  trul  37  eqcomx  47  ancoms  49  sylan  54  an32s  55  anassrs  57  ceq12  78  hbxfr  98