Theorem addcomli 9851

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 9850	. 2 |- ( B + A ) = ( A + B )
4		addcomli.2	. 2 |- ( A + B ) = C
5	3, 4	eqtri 2484	1 |- ( B + A ) = C

Syntax hints:   = wceq 1455   e. wcel 1898  (class class class)co 6315   CCcc 9563   + caddc 9568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6318  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-ltxr 9706

This theorem is referenced by:  mvlladdi  9918  negsubdi2i  9987  1p2e3  10763  4t4e16  11153  6t3e18  11158  6t5e30  11160  7t3e21  11163  7t4e28  11164  7t6e42  11166  7t7e49  11167  8t3e24  11169  8t4e32  11170  8t5e40  11171  8t8e64  11174  9t3e27  11176  9t4e36  11177  9t5e45  11178  9t6e54  11179  9t7e63  11180  9t8e72  11181  9t9e81  11182  4bc3eq4  12545  bpoly4  14161  bitsfzo  14458  gcdaddmlem  14541  6gcd4e2  14551  gcdi  15094  2exp8  15109  2exp16  15110  37prm  15141  43prm  15142  83prm  15143  139prm  15144  163prm  15145  317prm  15146  631prm  15147  1259lem1  15151  1259lem2  15152  1259lem3  15153  1259lem4  15154  1259lem5  15155  1259prm  15156  2503lem1  15157  2503lem2  15158  2503lem3  15159  2503prm  15160  4001lem1  15161  4001lem2  15162  4001lem4  15164  4001prm  15165  iaa  23330  dvradcnv  23425  eulerid  23478  binom4  23825  log2ublem3  23923  log2ub  23924  lgsdir2lem1  24300  m1lgs  24339  ex-ind-dvds  25948  vcm  26239  fib5  29287  fib6  29288  inductionexd  36638  lhe4.4ex1a  36722  dirkertrigeqlem1  37998  sqwvfoura  38130  sqwvfourb  38131  fourierswlem  38132  fouriersw  38133  gbpart8  38907