Theorem adantl 51

Description: Extract an assumption from the context.

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 50	. 2 ⊢ (R, S)⊧T
4	3	ancoms 49	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

This theorem is referenced by:  ct2  53  dedi  75  hbxfrf  97  notval2  149  ax4e  158  exlimd  171  alimdv  172  alnex  174  exnal1  175  isfree  176  dfex2  185  exmid  186  ax2  191  ax3  192  ax5  194  ax7  196  ax8  198  ax10  200  ax11  201  axext  206  axrep  207