Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > a1i | Unicode version |
Description: Change an empty context into any context. |
Ref | Expression |
---|---|
ax-trud.1 | |
ax-a1i.2 |
Ref | Expression |
---|---|
a1i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-trud.1 | . . 3 | |
2 | 1 | ax-trud 26 | . 2 |
3 | ax-a1i.2 | . 2 | |
4 | 2, 3 | syl 16 | 1 |
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 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 |