Theorem addid2 8045

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 7899	. . 3 |- 0 e. CC
2		addcom 8043	. . 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 8044	. 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 5850   CCcc 7759   0cc0 7761   + caddc 7764

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 7854  ax-icn 7856  ax-addcl 7857  ax-mulcl 7859  ax-addcom 7861  ax-i2m1 7866  ax-0id 7869

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

This theorem is referenced by:  readdcan  8046  addid2i  8049  addid2d  8056  cnegexlem1  8081  cnegexlem2  8082  addcan  8086  negneg  8156  fz0to4untppr  10067  fzoaddel2  10136  divfl0  10239  modqid  10292  sumrbdclem  11327  summodclem2a  11331  fisum0diag2  11397  eftlub  11640  gcdid  11928  ptolemy  13498