| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Alias for axaddcom 6428, for naming consistency with addcomi 6475. |
| Ref | Expression |
|---|---|
| addcom |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axaddcom 6428 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: addcomi 6475 addid2 6482 add12 6489 add23 6490 add42 6493 cnegexlem1 6499 cnegexlem3 6501 addcaniOLD 6506 addcan2 6508 subsub23 6533 addsub 6542 addsubOLD 6543 addsub12 6545 pncan2 6558 negsubdi2 6623 sub23 6630 nnncan1OLD 6633 sub4 6643 pnpcan2 6646 ppncan 6648 ltadd2 6807 leadd2 6809 ltsubadd2 6811 lesubadd2 6813 ltaddsub2 6815 leaddsub2 6817 leltadd 6830 addgtge0OLD 6836 ltaddpos2 6840 addge02 6862 conjmul 6975 recp1lt1 7084 recreclt 7085 nnleltp1 7138 nn0nnaddcl 7335 zaddcl 7374 zneo 7412 flzadd 7485 fzen 7664 fzshftral 7701 shftval2 7760 shftval4 7762 seqzval2 7796 subsq 7888 bernneq2 7900 rimul 7994 imre 8023 absmax 8149 fsumrev 8289 fsumshft 8291 bcxmas 8336 climshft2i 8366 climaddc2 8379 efaddlem14 8613 ef1tllem 8643 cosneg 8708 addcos 8724 sincossq 8726 cos2t 8728 absefi 8748 absefib 8750 demoivre 8752 nn0ennn 8766 ioo2bl 9190 cnaddabl 9434 addinv 9436 ipval2 9696 sineq0 10065 sineq0OLD 10066 hhph 10678 golem1 11843 stcltrlem1 11848 cdj3lem3b 12012 modaddabs 13612 dvdsaddr 13689 divalglem4 13699 divalgb 13707 gcdaddm 13735 truni1 14849 2wsms 15008 addsubeq4 15778 rddif 15798 fsumltisumi 15823 mettrifi2 15848 geomcau 15849 lincmb01cmp 15878 lincmb01icc 15879 haustlmu 15906 bfplem8 16005 rrntotbndlem2 16021 iccbnd 16026 pcorevlem 16086 addcomgi 16455 cnaddablNEW 17139 cnaddablxNEW 17140 zaddablxNEW 17141 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-fv 4014 df-opr 4886 df-oprab 4887 df-1st 5020 df-2nd 5021 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-plp 6240 df-ltp 6242 df-plpr 6316 df-enr 6318 df-nr 6319 df-plr 6320 df-c 6392 df-plus 6397 |