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 8027 | . 2 | |
4 | 1, 2, 3 | syl2anc 409 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 wcel 2135 (class class class)co 5837 cc 7743 caddc 7748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-addcom 7845 |
This theorem is referenced by: muladd11r 8046 comraddd 8047 subadd2 8094 pncan 8096 npcan 8099 subcan 8145 mvlladdd 8255 subaddeqd 8259 addrsub 8261 ltadd1 8319 leadd2 8321 ltsubadd2 8323 lesubadd2 8325 mulreim 8494 apadd2 8499 recp1lt1 8786 ltaddrp2d 9659 lincmb01cmp 9931 iccf1o 9932 rebtwn2zlemstep 10179 qavgle 10185 modqaddabs 10288 mulqaddmodid 10290 qnegmod 10295 modqadd2mod 10300 modqadd12d 10306 modqaddmulmod 10317 addmodlteq 10324 expaddzap 10490 bcn2m1 10672 bcn2p1 10673 remullem 10800 resqrexlemover 10939 maxabslemab 11135 maxabslemval 11137 bdtrilem 11167 climaddc2 11258 telfsumo 11394 fsumparts 11398 bcxmas 11417 isumshft 11418 cvgratnnlemsumlt 11456 cosneg 11655 sinadd 11664 sincossq 11676 cos2t 11678 absefi 11696 absefib 11698 gcdaddm 11903 pythagtrip 12201 metrtri 12935 apdifflemf 13777 apdiff 13779 |
Copyright terms: Public domain | W3C validator |