Colors of
variables: type var term |
Syntax hints: →
ht 2 ∗hb 3
kc 5 = ke 7
⊤kt 8 wffMMJ2t 12 |
This theorem was proved from axioms:
ax-cb1 29 ax-weq 40 ax-refl 42 |
This theorem is referenced by: tru
44 dedi
85 eqtru
86 hbth
109 hbov
111 ovl
117 wal
134 wan
136 alval
142 anval
148 alrimiv
151 dfan2
154 hbct
155 olc
164 orc
165 alrimi
182 exlimd
183 alnex
186 exnal1
187 dfex2
198 exmid
199 ax1
203 ax2
204 ax3
205 ax5
207 ax7
209 ax8
211 ax9
212 ax10
213 ax11
214 ax13
216 ax14
217 axext
219 axrep
220 axpow
221 axun
222 |