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

Theorem adantr 50
Description: Extract an assumption from the context.
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  51  ct1  52  sylan  54  an32s  55  anassrs  57  eqtru  76  hbxfr  98  hbov  101  hbct  145  imp  147  olc  154  orc  155  exlimdv2  156  exlimd  171  ax1  190  ax5  194  ax12  202  ax13  203  ax14  204
  Copyright terms: Public domain W3C validator