Theorem addcomli 9701

Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015.)

Hypotheses

Ref	Expression
mul.1	|- A e. CC
mul.2	|- B e. CC
addcomli.2	|- ( A + B ) = C

Assertion

Ref	Expression
addcomli	|- ( B + A ) = C

Proof of Theorem addcomli

Step	Hyp	Ref	Expression
1		mul.2	. . 3 |- B e. CC
2		mul.1	. . 3 |- A e. CC
3	1, 2	addcomi 9700	. 2 |- ( B + A ) = ( A + B )
4		addcomli.2	. 2 |- ( A + B ) = C
5	3, 4	eqtri 2421	1 |- ( B + A ) = C

Syntax hints:   = wceq 1399   e. wcel 1836  (class class class)co 6214   CCcc 9419   + caddc 9424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-resscn 9478  ax-1cn 9479  ax-icn 9480  ax-addcl 9481  ax-addrcl 9482  ax-mulcl 9483  ax-mulrcl 9484  ax-mulcom 9485  ax-addass 9486  ax-mulass 9487  ax-distr 9488  ax-i2m1 9489  ax-1ne0 9490  ax-1rid 9491  ax-rnegex 9492  ax-rrecex 9493  ax-cnre 9494  ax-pre-lttri 9495  ax-pre-lttrn 9496  ax-pre-ltadd 9497

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-nel 2590  df-ral 2747  df-rex 2748  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-po 4727  df-so 4728  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-ov 6217  df-er 7247  df-en 7454  df-dom 7455  df-sdom 7456  df-pnf 9559  df-mnf 9560  df-ltxr 9562

This theorem is referenced by:  mvlladdi  9768  negsubdi2i  9837  1p2e3  10595  4t4e16  10986  6t3e18  10991  6t5e30  10993  7t3e21  10996  7t4e28  10997  7t6e42  10999  7t7e49  11000  8t3e24  11002  8t4e32  11003  8t5e40  11004  8t8e64  11007  9t3e27  11009  9t4e36  11010  9t5e45  11011  9t6e54  11012  9t7e63  11013  9t8e72  11014  9t9e81  11015  bitsfzo  14106  gcdaddmlem  14187  gcdi  14580  2exp8  14595  2exp16  14596  37prm  14627  43prm  14628  83prm  14629  139prm  14630  163prm  14631  317prm  14632  631prm  14633  1259lem1  14634  1259lem2  14635  1259lem3  14636  1259lem4  14637  1259lem5  14638  1259prm  14639  2503lem1  14640  2503lem2  14641  2503lem3  14642  2503prm  14643  4001lem1  14644  4001lem2  14645  4001lem4  14647  4001prm  14648  iaa  22825  dvradcnv  22920  eulerid  22971  binom4  23316  log2ublem3  23414  log2ub  23415  lgsdir2lem1  23734  m1lgs  23773  ex-ind-dvds  25312  vcm  25602  fib5  28563  fib6  28564  4bc3eq4  29313  bpoly4  30010  lhe4.4ex1a  31438  dirkertrigeqlem1  32081  sqwvfoura  32212  sqwvfourb  32213  fourierswlem  32214  fouriersw  32215  inductionexd  38531