Theorem addcom 6458

Description: Alias for axaddcom 6428, for naming consistency with addcomi 6475.

Assertion

Ref	Expression
addcom	|- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))

Proof of Theorem addcom

Step	Hyp	Ref	Expression
1		axaddcom 6428	1 |- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  (class class class)co 4884  CCcc 6384   + caddc 6389

This theorem is referenced by:  addcomi 6475  addid2 6482  add12 6489  add23 6490  add42 6493  cnegexlem1 6499  cnegexlem3 6501  addcaniOLD 6506  addcan2 6508  subsub23 6533  addsub 6542  addsubOLD 6543  addsub12 6545  pncan2 6558  negsubdi2 6623  sub23 6630  nnncan1OLD 6633  sub4 6643  pnpcan2 6646  ppncan 6648  ltadd2 6807  leadd2 6809  ltsubadd2 6811  lesubadd2 6813  ltaddsub2 6815  leaddsub2 6817  leltadd 6830  addgtge0OLD 6836  ltaddpos2 6840  addge02 6862  conjmul 6975  recp1lt1 7084  recreclt 7085  nnleltp1 7138  nn0nnaddcl 7335  zaddcl 7374  zneo 7412  flzadd 7485  fzen 7664  fzshftral 7701  shftval2 7760  shftval4 7762  seqzval2 7796  subsq 7888  bernneq2 7900  rimul 7994  imre 8023  absmax 8149  fsumrev 8289  fsumshft 8291  bcxmas 8336  climshft2i 8366  climaddc2 8379  efaddlem14 8613  ef1tllem 8643  cosneg 8708  addcos 8724  sincossq 8726  cos2t 8728  absefi 8748  absefib 8750  demoivre 8752  nn0ennn 8766  ioo2bl 9190  cnaddabl 9434  addinv 9436  ipval2 9696  sineq0 10065  sineq0OLD 10066  hhph 10678  golem1 11843  stcltrlem1 11848  cdj3lem3b 12012  modaddabs 13612  dvdsaddr 13689  divalglem4 13699  divalgb 13707  gcdaddm 13735  truni1 14849  2wsms 15008  addsubeq4 15778  rddif 15798  fsumltisumi 15823  mettrifi2 15848  geomcau 15849  lincmb01cmp 15878  lincmb01icc 15879  haustlmu 15906  bfplem8 16005  rrntotbndlem2 16021  iccbnd 16026  pcorevlem 16086  addcomgi 16455  cnaddablNEW 17139  cnaddablxNEW 17140  zaddablxNEW 17141

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-plp 6240  df-ltp 6242  df-plpr 6316  df-enr 6318  df-nr 6319  df-plr 6320  df-c 6392  df-plus 6397

Copyright terms: Public domain