Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1541 (class class class)co 7349
1c1 10985 + caddc 10987 2c2 12141
3c3 12142 4c4 12143
6c6 12145 7c7 12146 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2708 ax-1cn 11042 ax-addcl 11044 ax-addass 11049 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-iota 6443 df-fv 6499 df-ov 7352 df-2 12149 df-3 12150
df-4 12151 df-5 12152
df-6 12153 df-7 12154 |
This theorem is referenced by: 4p4e8
12241 37prm
16927 317prm
16932 1259lem5
16941 2503lem2
16944 4001lem1
16947 4001lem2
16948 log2ub
26221 bposlem8
26561 2lgslem3d
26669 2lgsoddprmlem3d
26683 hgt750lem
33037 hgt750lem2
33038 fmtno5lem4
45497 257prm
45502 127prm
45540 gbpart7
45708 sbgoldbwt
45718 sbgoldbst
45719 ackval2012
46526 |