Theorem addlid 8218

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 8071	. . 3 |- 0 e. CC
2		addcom 8216	. . 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 8217	. 2 |- ( A e. CC -> ( A + 0 ) = A )
5	3, 4	eqtr3d 2241	1 |- ( A e. CC -> ( 0 + A ) = A )

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2177  (class class class)co 5951   CCcc 7930   0cc0 7932   + caddc 7935

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188  ax-1cn 8025  ax-icn 8027  ax-addcl 8028  ax-mulcl 8030  ax-addcom 8032  ax-i2m1 8037  ax-0id 8040

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  readdcan  8219  addlidi  8222  addlidd  8229  cnegexlem1  8254  cnegexlem2  8255  addcan  8259  negneg  8329  fz0to4untppr  10253  fzo0addel  10324  fzoaddel2  10326  divfl0  10446  modqid  10501  swrdspsleq  11128  swrds1  11129  sumrbdclem  11732  summodclem2a  11736  fisum0diag2  11802  eftlub  12045  gcdid  12351  cncrng  14375  ptolemy  15340