Theorem addcomd 7164

Description: Addition commutes. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) (Revised by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
muld.1	|- ( ph -> A e. CC )
addcomd.2	|- ( ph -> B e. CC )

Assertion

Ref	Expression
addcomd	|- ( ph -> ( A + B ) = ( B + A ) )

Proof of Theorem addcomd

Step	Hyp	Ref	Expression
1		muld.1	. 2 |- ( ph -> A e. CC )
2		addcomd.2	. 2 |- ( ph -> B e. CC )
3		addcom 7150	. 2 |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
4	1, 2, 3	syl2anc 391	1 |- ( ph -> ( A + B ) = ( B + A ) )

Syntax hints:   -> wi 4   = wceq 1243   e. wcel 1393  (class class class)co 5512   CCcc 6887   + caddc 6892

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101  ax-addcom 6984

This theorem is referenced by:  subadd2  7215  pncan  7217  npcan  7220  subcan  7266  ltadd1  7424  leadd2  7426  ltsubadd2  7428  lesubadd2  7430  mulreim  7595  apadd2  7600  recp1lt1  7865  ltaddrp2d  8657  lincmb01cmp  8871  iccf1o  8872  rebtwn2zlemstep  9107  expaddzap  9299  remullem  9471  resqrexlemover  9608  climaddc2  9850  clim2iser2  9858