This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem addcomli

Description: Addition commutes. (Contributed by Mario Carneiro, 19-Apr-2015)

Ref Expression
Hypotheses mul.1 
|- A e. CC
mul.2 
|- B e. CC
addcomli.2 
|- ( A + B ) = C
Assertion addcomli 
|- ( B + A ) = C

Proof

Step Hyp Ref Expression
1 mul.1 
 |-  A e. CC
2 mul.2 
 |-  B e. CC
3 addcomli.2 
 |-  ( A + B ) = C
4 2 1 addcomi 
 |-  ( B + A ) = ( A + B )
5 4 3 eqtri 
 |-  ( B + A ) = C