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

Theorem a1i 28
Description: Change an empty context into any context.
Hypotheses
Ref Expression
ax-trud.1 |- R:*
ax-a1i.2 |- T. |= A
Assertion
Ref Expression
a1i |- R |= A

Proof of Theorem a1i
StepHypRef Expression
1 ax-trud.1 . . 3 |- R:*
21ax-trud 26 . 2 |- R |= T.
3 ax-a1i.2 . 2 |- T. |= A
42, 3syl 16 1 |- R |= A
Colors of variables: type var term
Syntax hints:  *hb 3  T.kt 8   |= wffMMJ2 11  wffMMJ2t 12
This theorem was proved from axioms:  ax-syl 15  ax-trud 26
This theorem is referenced by:  eqcomx  47  dfov1  66  dfov2  67  eqid  73  eqtru  76  oveq123  88  hbl1  94  a17i  96  hbc  100  hbl  102  clf  105  ovl  107  ax4g  139  ax4  140  alrimiv  141  cla4v  142  pm2.21  143  dfan2  144  mpd  146  ex  148  notnot1  150  con2d  151  ecase  153  olc  154  orc  155  exlimdv2  156  exlimdv  157  ax4e  158  cla4ev  159  19.8a  160  cbvf  167  leqf  169  alrimi  170  exlimd  171  alnex  174  exnal1  175  ac  184  exmid  186  notnot  187  ax3  192  ax10  200  ax11  201  axext  206  axrep  207  axpow  208
  Copyright terms: Public domain W3C validator