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

Theorem a1i 28
Description: Change an empty context into any context. (Contributed by Mario Carneiro, 7-Oct-2014.)
Hypotheses
Ref Expression
ax-trud.1 R:∗
ax-a1i.2 ⊤⊧A
Assertion
Ref Expression
a1i RA

Proof of Theorem a1i
StepHypRef Expression
1 ax-trud.1 . . 3 R:∗
21ax-trud 26 . 2 R⊧⊤
3 ax-a1i.2 . 2 ⊤⊧A
42, 3syl 16 1 RA
Colors of variables: type var term
Syntax hints:  hb 3  kt 8  wffMMJ2 11  wffMMJ2t 12
This theorem was proved from axioms:  ax-syl 15  ax-trud 26
This theorem is referenced by:  eqcomx  52  dfov1  74  dfov2  75  eqid  83  eqtru  86  oveq123  98  hbl1  104  a17i  106  hbc  110  hbl  112  clf  115  ovl  117  ax4g  149  ax4  150  alrimiv  151  cla4v  152  pm2.21  153  dfan2  154  mpd  156  ex  158  notnot1  160  con2d  161  ecase  163  olc  164  orc  165  exlimdv2  166  exlimdv  167  ax4e  168  cla4ev  169  19.8a  170  cbvf  179  leqf  181  alrimi  182  exlimd  183  alnex  186  exnal1  187  ac  197  exmid  199  notnot  200  ax3  205  ax10  213  ax11  214  axext  219  axrep  220  axpow  221
  Copyright terms: Public domain W3C validator