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

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

This proof depends on axioms:  ax-syl 15  ax-jca 17

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