Colors of
variables: type var term |
Syntax hints: ∗hb 3 = ke 7
[kbr 9 wffMMJ2t 12 |
This theorem was proved from axioms:
ax-weq 40 ax-wov 71 |
This theorem is referenced by: clf
115 ovl
117 wal
134 wan
136 wim
137 weu
141 alval
142 exval
143 euval
144 notval
145 imval
146 orval
147 anval
148 pm2.21
153 dfan2
154 ecase
163 exlimdv2
166 exlimdv
167 ax4e
168 eta
178 cbvf
179 leqf
181 exlimd
183 ac
197 exmid
199 ax8
211 ax9
212 ax10
213 ax11
214 ax12
215 ax13
216 ax14
217 axext
219 axrep
220 axpow
221 axun
222 |