Theorem addid2 8058

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

Assertion

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

Proof of Theorem addid2

Step	Hyp	Ref	Expression
1		0cn 7912	. . 3 |- 0 e. CC
2		addcom 8056	. . 3 |- ( ( A e. CC /\ 0 e. CC ) -> ( A + 0 ) = ( 0 + A ) )
3	1, 2	mpan2 423	. 2 |- ( A e. CC -> ( A + 0 ) = ( 0 + A ) )
4		addid1 8057	. 2 |- ( A e. CC -> ( A + 0 ) = A )
5	3, 4	eqtr3d 2205	1 |- ( A e. CC -> ( 0 + A ) = A )

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   0cc0 7774   + caddc 7777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152  ax-1cn 7867  ax-icn 7869  ax-addcl 7870  ax-mulcl 7872  ax-addcom 7874  ax-i2m1 7879  ax-0id 7882

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  readdcan  8059  addid2i  8062  addid2d  8069  cnegexlem1  8094  cnegexlem2  8095  addcan  8099  negneg  8169  fz0to4untppr  10080  fzoaddel2  10149  divfl0  10252  modqid  10305  sumrbdclem  11340  summodclem2a  11344  fisum0diag2  11410  eftlub  11653  gcdid  11941  ptolemy  13539