Colors of
variables: type var term |
Syntax hints: hb 3
ke 7
kbr 9
kct 10 wffMMJ2 11 tan 119 tim 121 |
This theorem was proved from axioms:
ax-syl 15 ax-jca 17 ax-simpl 20 ax-simpr 21 ax-id 24 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-wctl 31 ax-wctr 32 ax-weq 40 ax-refl 42 ax-eqmp 45 ax-ded 46 ax-wct 47 ax-wc 49 ax-ceq 51 ax-wv 63 ax-wl 65
ax-beta 67 ax-distrc 68 ax-leq 69 ax-distrl 70 ax-wov 71 ax-eqtypi 77 ax-eqtypri 80 ax-hbl1 103 ax-17 105
ax-inst 113 |
This theorem depends on definitions:
df-ov 73 df-an 128 df-im 129 |
This theorem is referenced by: notval2
159 notnot1
160 con2d
161 ecase
163 olc
164 orc
165 exlimdv2
166 exlimdv
167 ax4e
168 exlimd
183 alnex
186 isfree
188 exmid
199 ax1
203 ax2
204 ax3
205 ax5
207 ax7
209 ax8
211 ax10
213 ax11
214 ax12
215 ax13
216 ax14
217 axext
219 axrep
220 axpow
221 axun
222 |