Colors of
variables: wff set class |
Syntax hints: class class
class wbr 3998 cc0 7786 c1 7787 cle 7967 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709
ax-5 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-13 2148 ax-14 2149 ax-ext 2157 ax-sep 4116 ax-pow 4169 ax-pr 4203 ax-un 4427 ax-setind 4530 ax-cnex 7877 ax-resscn 7878 ax-1re 7880 ax-addrcl 7883 ax-0lt1 7892 ax-rnegex 7895 ax-pre-ltirr 7898 ax-pre-lttrn 7900 |
This theorem depends on definitions:
df-bi 117 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1459 df-sb 1761 df-eu 2027 df-mo 2028 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-ne 2346 df-nel 2441 df-ral 2458 df-rex 2459 df-rab 2462 df-v 2737 df-dif 3129 df-un 3131 df-in 3133 df-ss 3140 df-pw 3574 df-sn 3595 df-pr 3596 df-op 3598 df-uni 3806 df-br 3999 df-opab 4060 df-xp 4626 df-cnv 4628 df-pnf 7968 df-mnf 7969 df-xr 7970 df-ltxr 7971 df-le 7972 |
This theorem is referenced by: lemulge11
8794 sup3exmid
8885 0le2
8980 1eluzge0
9545 0elunit
9955 1elunit
9956 fldiv4p1lem1div2
10273 q1mod
10324 expge0
10524 expge1
10525 faclbnd3
10689 sqrt1
11022 sqrt2gt1lt2
11025 abs1
11048 cvgratnnlembern
11498 fprodge0
11612 fprodge1
11614 ege2le3
11646 sinbnd
11727 cosbnd
11728 cos2bnd
11735 nn0oddm1d2
11880 flodddiv4
11905 sqnprm
12102 isprm5lem
12107 sqrt2irrap
12146 nn0sqrtelqelz
12172 pythagtriplem3
12233 sinhalfpilem
13705 zabsle1
13893 lgslem2
13895 lgsfcl2
13900 lgsdir2lem1
13922 lgsne0
13932 lgsdinn0
13942 trilpolemclim
14267 trilpolemlt1
14272 nconstwlpolemgt0
14294 |