Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 (class class class)co 7362
1c1 11059 + caddc 11061 2c2 12215
4c4 12217 5c5 12218
6c6 12219 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2708 ax-1cn 11116 ax-addcl 11118 ax-addass 11123 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rab 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-iota 6453 df-fv 6509 df-ov 7365 df-2 12223 df-3 12224
df-4 12225 df-5 12226
df-6 12227 |
This theorem is referenced by: 4p3e7
12314 div4p1lem1div2
12415 4t4e16
12724 6gcd4e2
16426 2exp16
16970 163prm
17004 631prm
17006 1259lem4
17013 2503lem2
17017 2503lem3
17018 4001lem1
17020 4001lem2
17021 4001lem4
17023 bposlem9
26656 hgt750lem2
33305 3exp7
40539 3lexlogpow5ineq1
40540 aks4d1p1p5
40561 235t711
40834 ex-decpmul
40835 3cubeslem3r
41039 lhe4.4ex1a
42683 fmtno4prmfac
45838 fmtno5faclem1
45845 gbowgt5
46028 mogoldbb
46051 |