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	⊢ R⊧A

Proof of Theorem a1i

Step	Hyp	Ref	Expression
1		ax-trud.1	. . 3 ⊢ R:∗
2	1	ax-trud 26	. 2 ⊢ R⊧⊤
3		ax-a1i.2	. 2 ⊢ ⊤⊧A
4	2, 3	syl 16	1 ⊢ R⊧A

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