Theorem adantl 56

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
adantl	|- (S, R) |= T

Proof of Theorem adantl

Step	Hyp	Ref	Expression
1		adantr.1	. . 3 |- R |= T
2		adantr.2	. . 3 |- S:*
3	1, 2	adantr 55	. 2 |- (R, S) |= T
4	3	ancoms 54	1 |- (S, R) |= T

Syntax hints:  *hb 3  kct 10   |= wffMMJ2 11  wffMMJ2t 12

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-cb1 29  ax-wctl 31  ax-wctr 32

This theorem is referenced by:  ct2  58  dedi  85  hbxfrf  107  notval2  159  ax4e  168  exlimd  183  alimdv  184  alnex  186  exnal1  187  isfree  188  dfex2  198  exmid  199  ax2  204  ax3  205  ax5  207  ax7  209  ax8  211  ax10  213  ax11  214  axext  219  axrep  220