| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Alias for axaddcom 5340, for naming consistency with addcomi 5387. |
| Ref | Expression |
|---|---|
| addcom |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axaddcom 5340 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: addcomi 5387 addid2 5394 add12 5401 add23 5402 add42 5404 cnegexlem1 5410 cnegexlem3 5412 addcani 5416 addcan2 5418 subsub23 5441 addsub 5449 addsub12 5451 pncan2 5463 negsubdi2 5523 sub23 5530 nnncan1 5532 sub4 5541 pnpcan2 5544 ppncan 5546 ltadd2 5689 leadd2 5691 ltsubadd2 5693 lesubadd2 5695 ltaddsub2 5697 leaddsub2 5699 leltadd 5711 addgtge0 5714 ltaddpos2 5717 addge02 5738 conjmul 5855 recp1lt1 5961 recreclt 5962 nnleltp1 6015 nn0nnaddcl 6208 zaddcl 6247 zneo 6285 fzshftral 6548 shftval2 6606 shftval4 6608 seqzval2 6642 subsq 6731 bernneq2 6742 rimul 6834 imre 6863 absmax 6987 fsumrev 7119 fsumshf 7121 bcxmas 7166 climshft2i 7196 climaddc2 7209 efaddlem14 7441 ef1tllem 7471 cosneg 7534 addcos 7550 sincossq 7552 cos2t 7554 absefi 7574 demoivre 7576 nn0ennn 7589 ioo2bl 7997 cnaddabl 8210 addinv 8212 ipval2 8441 sineq0 8796 hhph 9128 golem1 10282 stcltrlem1 10287 cdj3lem3b 10451 truni1 10593 2wsms 10712 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1003 ax-gen 1004 ax-8 1005 ax-9 1006 ax-10 1007 ax-11 1008 ax-12 1009 ax-13 1010 ax-14 1011 ax-17 1012 ax-4 1014 ax-5o 1016 ax-6o 1019 ax-9o 1164 ax-10o 1182 ax-16 1252 ax-11o 1260 ax-ext 1504 ax-rep 2748 ax-sep 2758 ax-nul 2765 ax-pow 2798 ax-pr 2835 ax-un 2922 ax-inf2 4687 |
| This theorem depends on definitions: df-bi 154 df-or 231 df-an 232 df-3or 788 df-3an 789 df-ex 1022 df-sb 1214 df-eu 1424 df-mo 1425 df-clab 1510 df-cleq 1515 df-clel 1518 df-ne 1634 df-ral 1696 df-rex 1697 df-reu 1698 df-rab 1699 df-v 1859 df-sbc 1989 df-csb 2052 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-pss 2106 df-nul 2332 df-if 2414 df-pw 2454 df-sn 2464 df-pr 2465 df-tp 2467 df-op 2468 df-uni 2558 df-int 2588 df-iun 2622 df-br 2675 df-opab 2722 df-tr 2736 df-eprel 2888 df-id 2891 df-po 2896 df-so 2906 df-fr 2974 df-we 2991 df-ord 3008 df-on 3009 df-lim 3010 df-suc 3011 df-om 3189 df-xp 3241 df-rel 3242 df-cnv 3243 df-co 3244 df-dm 3245 df-rn 3246 df-res 3247 df-ima 3248 df-fun 3249 df-fn 3250 df-f 3251 df-fv 3255 df-rdg 3990 df-opr 4023 df-oprab 4024 df-1st 4137 df-2nd 4138 df-1o 4191 df-oadd 4193 df-omul 4194 df-er 4319 df-ec 4321 df-qs 4324 df-ni 5065 df-pli 5066 df-mi 5067 df-lti 5068 df-plpq 5100 df-mpq 5101 df-enq 5102 df-nq 5103 df-plq 5104 df-mq 5105 df-rq 5106 df-ltq 5107 df-1q 5108 df-np 5151 df-plp 5153 df-ltp 5155 df-plpr 5229 df-enr 5231 df-nr 5232 df-plr 5233 df-c 5305 df-plus 5310 |