Theorem adantr 55

Description: Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)

Hypotheses

Ref	Expression
adantr.1	⊢ R⊧T
adantr.2	⊢ S:∗

Assertion

Ref	Expression
adantr	⊢ (R, S)⊧T

Proof of Theorem adantr

Step	Hyp	Ref	Expression
1		adantr.1	. . . 4 ⊢ R⊧T
2	1	ax-cb1 29	. . 3 ⊢ R:∗
3		adantr.2	. . 3 ⊢ S:∗
4	2, 3	simpl 22	. 2 ⊢ (R, S)⊧R
5	4, 1	syl 16	1 ⊢ (R, S)⊧T

Syntax hints:  ∗hb 3  kct 10  ⊧wffMMJ2 11  wffMMJ2t 12

This theorem was proved from axioms:  ax-syl 15  ax-simpl 20  ax-cb1 29

This theorem is referenced by:  adantl  56  ct1  57  sylan  59  an32s  60  anassrs  62  eqtru  86  hbxfr  108  hbov  111  hbct  155  imp  157  olc  164  orc  165  exlimdv2  166  exlimd  183  ax1  203  ax5  207  ax12  215  ax13  216  ax14  217