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

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
StepHypRef Expression
1 adantr.1 . . . 4 |- R |= T
21ax-cb1 29 . . 3 |- R:*
3 adantr.2 . . 3 |- S:*
42, 3simpl 22 . 2 |- (R, S) |= R
54, 1syl 16 1 |- (R, S) |= 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-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
  Copyright terms: Public domain W3C validator