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

Theorem simpr 23
Description: Extract an assumption from the context. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
ax-simpl.1 R:∗
ax-simpl.2 S:∗
Assertion
Ref Expression
simpr (R, S)⊧S

Proof of Theorem simpr
StepHypRef Expression
1 ax-simpl.1 . 2 R:∗
2 ax-simpl.2 . 2 S:∗
31, 2ax-simpr 21 1 (R, S)⊧S
Colors of variables: type var term
Syntax hints:  hb 3  kct 10  wffMMJ2 11  wffMMJ2t 12
This theorem was proved from axioms:  ax-simpr 21
This theorem is referenced by:  simprd  38  ancoms  54  ct1  57  sylan  59  an32s  60  anassrs  62  dfan2  154  imp  157  ex  158  notval2  159  notnot1  160  olc  164  orc  165  exlimdv2  166  exlimd  183  exmid  199  notnot  200  ax1  203  ax2  204  ax3  205  ax8  211  ax11  214  ax13  216  ax14  217
  Copyright terms: Public domain W3C validator