Theorem addlid 8428

Description: 0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)

Assertion

Ref	Expression
addlid	|- ( A e. CC -> ( 0 + A ) = A )

Proof of Theorem addlid

Step	Hyp	Ref	Expression
1		0cn 8282	. . 3 |- 0 e. CC
2		addcom 8426	. . 3 |- ( ( A e. CC /\ 0 e. CC ) -> ( A + 0 ) = ( 0 + A ) )
3	1, 2	mpan2 425	. 2 |- ( A e. CC -> ( A + 0 ) = ( 0 + A ) )
4		addrid 8427	. 2 |- ( A e. CC -> ( A + 0 ) = A )
5	3, 4	eqtr3d 2269	1 |- ( A e. CC -> ( 0 + A ) = A )

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   0cc0 8143   + caddc 8146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-addcom 8243  ax-i2m1 8248  ax-0id 8251

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-clel 2230

This theorem is referenced by:  readdcan  8429  addlidi  8432  addlidd  8439  cnegexlem1  8464  cnegexlem2  8465  addcan  8469  negneg  8539  fz0to4untppr  10480  fzo0addel  10555  fzoaddel2  10557  divfl0  10680  modqid  10735  swrdspsleq  11384  swrds1  11385  sumrbdclem  12088  summodclem2a  12092  fisum0diag2  12158  eftlub  12401  gcdid  12707  cncrng  14829  ptolemy  15801