Theorem sylan 59

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

Hypotheses

Ref	Expression
sylan.1	⊢ R⊧S
sylan.2	⊢ (S, T)⊧A

Assertion

Ref	Expression
sylan	⊢ (R, T)⊧A

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.1	. . 3 ⊢ R⊧S
2		sylan.2	. . . . 5 ⊢ (S, T)⊧A
3	2	ax-cb1 29	. . . 4 ⊢ (S, T):∗
4	3	wctr 34	. . 3 ⊢ T:∗
5	1, 4	adantr 55	. 2 ⊢ (R, T)⊧S
6	1	ax-cb1 29	. . 3 ⊢ R:∗
7	6, 4	simpr 23	. 2 ⊢ (R, T)⊧T
8	5, 7, 2	syl2anc 19	1 ⊢ (R, T)⊧A

This proof depends on syntax axioms:  kct 10  ⊧wffMMJ2 11

This proof depends on axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-cb1 29  ax-wctr 32

This theorem is used by:  anasss  61