Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcom Structured version   Unicode version

 Description: Addition commutes. This used to be one of our complex number axioms, until it was found to be dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression

StepHypRef Expression
1 1cnd 9658 . . . . . . . 8
21, 1addcld 9661 . . . . . . 7
3 simpl 458 . . . . . . 7
4 simpr 462 . . . . . . 7
52, 3, 4adddid 9666 . . . . . 6
63, 4addcld 9661 . . . . . . 7
7 1p1times 9803 . . . . . . 7
86, 7syl 17 . . . . . 6
9 1p1times 9803 . . . . . . 7
10 1p1times 9803 . . . . . . 7
119, 10oveqan12d 6324 . . . . . 6
125, 8, 113eqtr3rd 2479 . . . . 5
133, 3addcld 9661 . . . . . 6
1413, 4, 4addassd 9664 . . . . 5
156, 3, 4addassd 9664 . . . . 5
1612, 14, 153eqtr4d 2480 . . . 4
1713, 4addcld 9661 . . . . 5
186, 3addcld 9661 . . . . 5
19 addcan2 9817 . . . . 5
2017, 18, 4, 19syl3anc 1264 . . . 4
2116, 20mpbid 213 . . 3
223, 3, 4addassd 9664 . . 3
233, 4, 3addassd 9664 . . 3
2421, 22, 233eqtr3d 2478 . 2
254, 3addcld 9661 . . 3
26 addcan 9816 . . 3
273, 6, 25, 26syl3anc 1264 . 2
2824, 27mpbid 213 1