Colors of
variables: type var term |
Syntax hints: ht 2 kc 5
ke 7
kbr 9
wffMMJ2 11 wffMMJ2t 12 |
This theorem was proved from axioms:
ax-syl 15 ax-jca 17 ax-trud 26 ax-cb1 29 ax-cb2 30 ax-weq 40 ax-refl 42 ax-eqmp 45 ax-wc 49 ax-ceq 51 ax-wov 71 ax-eqtypi 77 |
This theorem depends on definitions:
df-ov 73 |
This theorem is referenced by: eqtri
95 clf
115 exval
143 euval
144 orval
147 exlimdv2
166 exlimdv
167 ax4e
168 cbvf
179 leqf
181 exlimd
183 ac
197 exmid
199 exnal
201 ax9
212 ax10
213 ax11
214 ax13
216 axrep
220 axpow
221 axun
222 |