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

Theorem addcomi 9000
Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
Hypotheses
Ref Expression
mul.1  |-  A  e.  CC
mul.2  |-  B  e.  CC
Assertion
Ref Expression
addcomi  |-  ( A  +  B )  =  ( B  +  A
)

Proof of Theorem addcomi
StepHypRef Expression
1 mul.1 . 2  |-  A  e.  CC
2 mul.2 . 2  |-  B  e.  CC
3 addcom 8995 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  +  B
)  =  ( B  +  A ) )
41, 2, 3mp2an 655 1  |-  ( A  +  B )  =  ( B  +  A
)
Colors of variables: wff set class
Syntax hints:    = wceq 1625    e. wcel 1687  (class class class)co 5821   CCcc 8732    + caddc 8737
This theorem is referenced by:  addcomli  9001  add42i  9029  fztpval  10841  binom2aiOLD  11209  0.999...  12333  ef01bndlem  12460  bitsfzo  12622  modxai  13079  pcoass  18518  iblitg  19119  tangtx  19869  eff1o  19907  ang180lem2  20104  log2ublem2  20239  log2ublem3  20240  basellem9  20322  ppiub  20439  bposlem8  20526  lgsdir2lem1  20558  lgsdir2lem2  20559  lgsdir2lem3  20560  lgsdir2lem5  20562  ipasslem10  21411  normlem2  21684  normlem3  21685  norm-ii-i  21710  normpar2i  21729  ax5seglem7  23972  axlowdimlem16  23994  2eq3m1  24580  fdc  25856  rabren3dioph  26299  stoweidlem13  27163
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-sep 4144  ax-nul 4152  ax-pow 4189  ax-pr 4215  ax-un 4513  ax-resscn 8791  ax-1cn 8792  ax-icn 8793  ax-addcl 8794  ax-addrcl 8795  ax-mulcl 8796  ax-mulrcl 8797  ax-mulcom 8798  ax-addass 8799  ax-mulass 8800  ax-distr 8801  ax-i2m1 8802  ax-1ne0 8803  ax-1rid 8804  ax-rnegex 8805  ax-rrecex 8806  ax-cnre 8807  ax-pre-lttri 8808  ax-pre-lttrn 8809  ax-pre-ltadd 8810
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 937  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-eu 2150  df-mo 2151  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-nel 2452  df-ral 2551  df-rex 2552  df-rab 2555  df-v 2793  df-sbc 2995  df-csb 3085  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-nul 3459  df-if 3569  df-pw 3630  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3831  df-br 4027  df-opab 4081  df-mpt 4082  df-id 4310  df-po 4315  df-so 4316  df-xp 4696  df-rel 4697  df-cnv 4698  df-co 4699  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fun 5225  df-fn 5226  df-f 5227  df-f1 5228  df-fo 5229  df-f1o 5230  df-fv 5231  df-ov 5824  df-er 6657  df-en 6861  df-dom 6862  df-sdom 6863  df-pnf 8866  df-mnf 8867  df-ltxr 8869
  Copyright terms: Public domain W3C validator