Colors of
variables: wff
setvar class |
Syntax hints: = wceq 1395 class class class wbr 4452 |
This theorem is referenced by: 1lt2nq
9372 0lt1sr
9493 declt
11025 decltc
11026 fzennn
12078 faclbnd4lem1
12371 fsumabs
13615 ovolfiniun
21912 log2ublem3
23279 log2ub
23280 emgt0
23336 bclbnd
23555 bposlem8
23566 nmblolbii
25714 normlem6
26032 norm-ii-i
26054 nmbdoplbi
26943 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704
ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions:
df-bi 185 df-or 370
df-an 371 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-rab 2816 df-v 3111 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-nul 3785 df-if 3942 df-sn 4030 df-pr 4032 df-op 4036 df-br 4453 |