Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addcomd | Unicode version |
Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
muld.1 | |
addcomd.2 |
Ref | Expression |
---|---|
addcomd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 | . 2 | |
2 | addcomd.2 | . 2 | |
3 | addcom 7899 | . 2 | |
4 | 1, 2, 3 | syl2anc 408 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 wcel 1480 (class class class)co 5774 cc 7618 caddc 7623 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-addcom 7720 |
This theorem is referenced by: muladd11r 7918 comraddd 7919 subadd2 7966 pncan 7968 npcan 7971 subcan 8017 mvlladdd 8127 subaddeqd 8131 addrsub 8133 ltadd1 8191 leadd2 8193 ltsubadd2 8195 lesubadd2 8197 mulreim 8366 apadd2 8371 recp1lt1 8657 ltaddrp2d 9518 lincmb01cmp 9786 iccf1o 9787 rebtwn2zlemstep 10030 qavgle 10036 modqaddabs 10135 mulqaddmodid 10137 qnegmod 10142 modqadd2mod 10147 modqadd12d 10153 modqaddmulmod 10164 addmodlteq 10171 expaddzap 10337 bcn2m1 10515 bcn2p1 10516 remullem 10643 resqrexlemover 10782 maxabslemab 10978 maxabslemval 10980 bdtrilem 11010 climaddc2 11099 telfsumo 11235 fsumparts 11239 bcxmas 11258 isumshft 11259 cvgratnnlemsumlt 11297 cosneg 11434 sinadd 11443 sincossq 11455 cos2t 11457 absefi 11475 absefib 11477 gcdaddm 11672 metrtri 12546 |
Copyright terms: Public domain | W3C validator |