HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  adantl Unicode version

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
StepHypRef Expression
1 adantr.1 . . 3 |- R |= T
2 adantr.2 . . 3 |- S:*
31, 2adantr 55 . 2 |- (R, S) |= T
43ancoms 54 1 |- (S, R) |= T
Colors of variables: type var term
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
  Copyright terms: Public domain W3C validator