Theorem syldan 36

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

Hypotheses

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

Assertion

Ref	Expression
syldan	⊢ (R, S)⊧A

Proof of Theorem syldan

Step	Hyp	Ref	Expression
1		syldan.1	. . . . 5 ⊢ (R, S)⊧T
2	1	ax-cb1 29	. . . 4 ⊢ (R, S):∗
3	2	wctl 33	. . 3 ⊢ R:∗
4	2	wctr 34	. . 3 ⊢ S:∗
5	3, 4	simpl 22	. 2 ⊢ (R, S)⊧R
6		syldan.2	. 2 ⊢ (R, T)⊧A
7	5, 1, 6	syl2anc 19	1 ⊢ (R, S)⊧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-cb1 29  ax-wctl 31  ax-wctr 32

This theorem is used by:  alimdv  184