Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcomd Structured version   Visualization version   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.)
Hypotheses
Ref Expression
muld.1
Assertion
Ref Expression

StepHypRef Expression
1 1cnd 9656 . . . . . . . 8
21, 1addcld 9659 . . . . . . 7
3 muld.1 . . . . . . 7
4 addcomd.2 . . . . . . 7
52, 3, 4adddid 9664 . . . . . 6
63, 4addcld 9659 . . . . . . 7
7 1p1times 9801 . . . . . . 7
86, 7syl 17 . . . . . 6
9 1p1times 9801 . . . . . . . 8
103, 9syl 17 . . . . . . 7
11 1p1times 9801 . . . . . . . 8
124, 11syl 17 . . . . . . 7
1310, 12oveq12d 6306 . . . . . 6
145, 8, 133eqtr3rd 2493 . . . . 5
153, 3addcld 9659 . . . . . 6
1615, 4, 4addassd 9662 . . . . 5
176, 3, 4addassd 9662 . . . . 5
1814, 16, 173eqtr4d 2494 . . . 4
1915, 4addcld 9659 . . . . 5
206, 3addcld 9659 . . . . 5
21 addcan2 9815 . . . . 5
2219, 20, 4, 21syl3anc 1267 . . . 4
2318, 22mpbid 214 . . 3
243, 3, 4addassd 9662 . . 3
253, 4, 3addassd 9662 . . 3
2623, 24, 253eqtr3d 2492 . 2
274, 3addcld 9659 . . 3
28 addcan 9814 . . 3
293, 6, 27, 28syl3anc 1267 . 2
3026, 29mpbid 214 1