![]() |
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 8092 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 411 |
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 108 ax-addcom 7910 |
This theorem is referenced by: muladd11r 8111 comraddd 8112 subadd2 8159 pncan 8161 npcan 8164 subcan 8210 mvlladdd 8320 subaddeqd 8324 addrsub 8326 ltadd1 8384 leadd2 8386 ltsubadd2 8388 lesubadd2 8390 mulreim 8559 apadd2 8564 recp1lt1 8854 ltaddrp2d 9729 lincmb01cmp 10001 iccf1o 10002 rebtwn2zlemstep 10250 qavgle 10256 modqaddabs 10359 mulqaddmodid 10361 qnegmod 10366 modqadd2mod 10371 modqadd12d 10377 modqaddmulmod 10388 addmodlteq 10395 expaddzap 10561 bcn2m1 10744 bcn2p1 10745 remullem 10875 resqrexlemover 11014 maxabslemab 11210 maxabslemval 11212 bdtrilem 11242 climaddc2 11333 telfsumo 11469 fsumparts 11473 bcxmas 11492 isumshft 11493 cvgratnnlemsumlt 11531 cosneg 11730 sinadd 11739 sincossq 11751 cos2t 11753 absefi 11771 absefib 11773 gcdaddm 11979 pythagtrip 12277 mulgnndir 12965 mulgdirlem 12967 metrtri 13770 2sqlem3 14346 apdifflemf 14676 apdiff 14678 |
Copyright terms: Public domain | W3C validator |