Theorem addass 5337

Description: Associative law for addition.

Hypotheses

Ref	Expression
axi.1	|- A e. CC
axi.2	|- B e. CC
axi.3	|- C e. CC

Assertion

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

Proof of Theorem addass

Step	Hyp	Ref	Expression
1		axi.1	. 2 |- A e. CC
2		axi.2	. 2 |- B e. CC
3		axi.3	. 2 |- C e. CC
4		axaddass 5290	. 2 |- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) + C) = (A + (B + C)))
5	1, 2, 3, 4	mp3an 920	1 |- ((A + B) + C) = (A + (B + C))

Syntax hints:   = wceq 960   e. wcel 962  (class class class)co 3977  CCcc 5245   + caddc 5250

This theorem is referenced by:  negsub 5394  negneg 5403  ltsubadd 5607  ltneg 5616  ixi 5694  2p2e4 6007  3p2e5 6013  3p3e6 6014  4p2e6 6015  4p3e7 6016  4p4e8 6017  5p2e7 6018  5p3e8 6019  5p4e9 6020  5p5e10 6021  6p2e8 6022  6p3e9 6023  6p4e10 6024  7p2e9 6025  7p3e10 6026  8p2e10 6027  binom2 6657  discrlem1 6670  sqrlem16 6702  faclbnd4lem1 6962  fnsmnt 7240  eirrlem3 7405  efsep 7410  cos2bnd 7490  ruclem2 7526  ruclem30 7554  normlem3 8985  projlem3 9195  stadd3 10183

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-rep 2706  ax-sep 2716  ax-nul 2723  ax-pow 2756  ax-pr 2793  ax-un 2880  ax-inf2 4637

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2010  df-dif 2058  df-un 2059  df-in 2060  df-ss 2062  df-pss 2064  df-nul 2290  df-if 2372  df-pw 2412  df-sn 2422  df-pr 2423  df-tp 2425  df-op 2426  df-uni 2516  df-int 2546  df-iun 2580  df-br 2633  df-opab 2680  df-tr 2694  df-eprel 2846  df-id 2849  df-po 2854  df-so 2864  df-fr 2931  df-we 2948  df-ord 2965  df-on 2966  df-lim 2967  df-suc 2968  df-om 3146  df-xp 3198  df-rel 3199  df-cnv 3200  df-co 3201  df-dm 3202  df-rn 3203  df-res 3204  df-ima 3205  df-fun 3206  df-fn 3207  df-f 3208  df-fv 3212  df-rdg 3946  df-opr 3979  df-oprab 3980  df-1st 4093  df-2nd 4094  df-1o 4147  df-oadd 4149  df-omul 4150  df-er 4275  df-ec 4277  df-qs 4280  df-ni 5013  df-pli 5014  df-mi 5015  df-lti 5016  df-plpq 5048  df-mpq 5049  df-enq 5050  df-nq 5051  df-plq 5052  df-mq 5053  df-rq 5054  df-ltq 5055  df-1q 5056  df-np 5099  df-plp 5101  df-ltp 5103  df-plpr 5177  df-enr 5179  df-nr 5180  df-plr 5181  df-c 5253  df-plus 5258

Copyright terms: Public domain