Metamath Proof Explorer


Theorem comraddi

Description: Commute RHS addition. See addcomli to commute addition on LHS. (Contributed by David A. Wheeler, 11-Oct-2018)

Ref Expression
Hypotheses comraddi.1 B
comraddi.2 C
comraddi.3 A = B + C
Assertion comraddi A = C + B

Proof

Step Hyp Ref Expression
1 comraddi.1 B
2 comraddi.2 C
3 comraddi.3 A = B + C
4 1 2 addcomi B + C = C + B
5 3 4 eqtri A = C + B