Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  addcom 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

Proof of Theorem addcom
StepHypRef Expression
1 ax-1cn 8675 . . . . . . . . 9
21a1i 12 . . . . . . . 8
32, 2addcld 8734 . . . . . . 7
4 simpl 445 . . . . . . 7
5 simpr 449 . . . . . . 7
63, 4, 5adddid 8739 . . . . . 6
74, 5addcld 8734 . . . . . . 7
8 1p1times 8863 . . . . . . 7
97, 8syl 17 . . . . . 6
10 1p1times 8863 . . . . . . 7
11 1p1times 8863 . . . . . . 7
1210, 11oveqan12d 5729 . . . . . 6
136, 9, 123eqtr3rd 2294 . . . . 5
144, 4addcld 8734 . . . . . 6
1514, 5, 5addassd 8737 . . . . 5
167, 4, 5addassd 8737 . . . . 5
1713, 15, 163eqtr4d 2295 . . . 4
1814, 5addcld 8734 . . . . 5
197, 4addcld 8734 . . . . 5
20 addcan2 8877 . . . . 5
2118, 19, 5, 20syl3anc 1187 . . . 4
2217, 21mpbid 203 . . 3
234, 4, 5addassd 8737 . . 3
244, 5, 4addassd 8737 . . 3
2522, 23, 243eqtr3d 2293 . 2
265, 4addcld 8734 . . 3
27 addcan 8876 . . 3
284, 7, 26, 27syl3anc 1187 . 2
2925, 28mpbid 203 1