Colors of
variables: wff
setvar class |
Syntax hints: -> wi 4 /\ w3a 965
= wceq 1370 e. wcel 1757 (class class class)co 6174
cc 9365 caddc 9370 cmin 9680 |
This theorem is referenced by: addsub
9706 subadd23
9707 addsubeq4
9710 npncan
9715 subsub
9724 subsub3
9726 addsub4
9737 negsub
9742 addsubassi
9784 addsubassd
9824 zeo
10812 fzen2
11876 odd2np1
13678 chtub
22651 axcontlem2
23330 fsumcube
28321 stoweidlem26
29943 numclwwlkovf2ex
30801 numclwlk2lem2f
30818 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671
ax-6 1709 ax-7 1729 ax-8 1759
ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2429 ax-sep 4495 ax-nul 4503 ax-pow 4552 ax-pr 4613 ax-un 6456 ax-resscn 9424 ax-1cn 9425 ax-icn 9426 ax-addcl 9427 ax-addrcl 9428 ax-mulcl 9429 ax-mulrcl 9430 ax-mulcom 9431 ax-addass 9432 ax-mulass 9433 ax-distr 9434 ax-i2m1 9435 ax-1ne0 9436 ax-1rid 9437 ax-rnegex 9438 ax-rrecex 9439 ax-cnre 9440 ax-pre-lttri 9441 ax-pre-lttrn 9442 ax-pre-ltadd 9443 |
This theorem depends on definitions:
df-bi 185 df-or 370
df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1702 df-eu 2263 df-mo 2264 df-clab 2436 df-cleq 2442 df-clel 2445 df-nfc 2598 df-ne 2643 df-nel 2644 df-ral 2797 df-rex 2798 df-reu 2799 df-rab 2801 df-v 3054 df-sbc 3269 df-csb 3371 df-dif 3413 df-un 3415 df-in 3417 df-ss 3424 df-nul 3720 df-if 3874 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4174 df-br 4375 df-opab 4433 df-mpt 4434 df-id 4718 df-po 4723 df-so 4724 df-xp 4928 df-rel 4929 df-cnv 4930 df-co 4931 df-dm 4932 df-rn 4933 df-res 4934 df-ima 4935 df-iota 5463 df-fun 5502 df-fn 5503 df-f 5504 df-f1 5505 df-fo 5506 df-f1o 5507 df-fv 5508 df-riota 6135 df-ov 6177 df-oprab 6178 df-mpt2 6179 df-er 7185 df-en 7395 df-dom 7396 df-sdom 7397 df-pnf 9505 df-mnf 9506 df-ltxr 9508 df-sub 9682 |