HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Identity law for addition. |
| Ref | Expression |
|---|---|
| addid1.1 |
    |
| Ref | Expression |
|---|---|
| addid1 |
 
   |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | addid1.1 |
. 2
| |
| 2 | ax0id 5261 |
. 2
 | |
| 3 | 1, 2 | ax-mp 7 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wceq 954 wcel 956 (class class class)co 3954
cc 5212
cc0 5214
caddc 5217 |
| This theorem is referenced by: negsub 5361 negneg 5370 1re 5415 ltsubadd 5576 addgt0 5580 addge0 5581 add20 5584 ltneg 5585 lesub0 5594 ixi 5662 recextlem2 5664 nn0addclt 6075 sumsqne0 6573 bernneq 6591 nnesq 6600 sqrlem1 6611 sqrlem15 6625 crulem 6674 rereb 6723 addcj 6741 faclbnd4lem3 6895 bcpasc 6915 infcvglem2 7165 geolimilem 7178 ef0lem 7260 demoivre 7434 dscmet 7870 vc0 8140 ip0r 8317 ip2i 8431 pythi 8454 minveclem30 8518 sinhalfpilem 8617 eulerid 8621 sinperlem1 8624 efper 8686 normlem6 8920 normpyth 8948 normpar 8960 ocsh 9095 pjnel 9608 0lnfn 9848 lnopeq0 9870 nlelsh 9931 unierr 9975 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861 ax-inf2 4605 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2499 df-int 2529 df-iun 2563 df-br 2615 df-opab 2662 df-tr 2676 df-eprel 2827 df-id 2830 df-po 2835 df-so 2845 df-fr 2912 df-we 2929 df-ord 2946 df-on 2947 df-lim 2948 df-suc 2949 df-om 3127 df-xp 3179 df-rel 3180 df-cnv 3181 df-co 3182 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fun 3187 df-fn 3188 df-f 3189 df-fv 3193 df-rdg 3923 df-opr 3956 df-oprab 3957 df-1st 4069 df-2nd 4070 df-1o 4123 df-oadd 4125 df-omul 4126 df-er 4251 df-ec 4253 df-qs 4256 df-ni 4980 df-pli 4981 df-mi 4982 df-lti 4983 df-plpq 5015 df-mpq 5016 df-enq 5017 df-nq 5018 df-plq 5019 df-mq 5020 df-rq 5021 df-ltq 5022 df-1q 5023 df-np 5066 df-1p 5067 df-plp 5068 df-ltp 5070 df-plpr 5144 df-enr 5146 df-nr 5147 df-plr 5148 df-0r 5151 df-c 5220 df-0 5221 df-plus 5225 |