![]() |
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 7923 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 409 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 ax-addcom 7744 |
This theorem is referenced by: muladd11r 7942 comraddd 7943 subadd2 7990 pncan 7992 npcan 7995 subcan 8041 mvlladdd 8151 subaddeqd 8155 addrsub 8157 ltadd1 8215 leadd2 8217 ltsubadd2 8219 lesubadd2 8221 mulreim 8390 apadd2 8395 recp1lt1 8681 ltaddrp2d 9548 lincmb01cmp 9816 iccf1o 9817 rebtwn2zlemstep 10061 qavgle 10067 modqaddabs 10166 mulqaddmodid 10168 qnegmod 10173 modqadd2mod 10178 modqadd12d 10184 modqaddmulmod 10195 addmodlteq 10202 expaddzap 10368 bcn2m1 10547 bcn2p1 10548 remullem 10675 resqrexlemover 10814 maxabslemab 11010 maxabslemval 11012 bdtrilem 11042 climaddc2 11131 telfsumo 11267 fsumparts 11271 bcxmas 11290 isumshft 11291 cvgratnnlemsumlt 11329 cosneg 11470 sinadd 11479 sincossq 11491 cos2t 11493 absefi 11511 absefib 11513 gcdaddm 11708 metrtri 12585 apdifflemf 13414 apdiff 13416 |
Copyright terms: Public domain | W3C validator |