Metamath Proof Explorer


Theorem decaddcom

Description: Commute ones place in addition. (Contributed by Steven Nguyen, 29-Jan-2023)

Ref Expression
Hypotheses decaddcom.a A 0
decaddcom.b B 0
decaddcom.c C 0
Assertion decaddcom Could not format assertion : No typesetting found for |- ( ; A B + C ) = ( ; A C + B ) with typecode |-

Proof

Step Hyp Ref Expression
1 decaddcom.a A 0
2 decaddcom.b B 0
3 decaddcom.c C 0
4 eqid Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |-
5 eqid B + C = B + C
6 1 2 3 4 5 decaddi Could not format ( ; A B + C ) = ; A ( B + C ) : No typesetting found for |- ( ; A B + C ) = ; A ( B + C ) with typecode |-
7 eqid Could not format ; A C = ; A C : No typesetting found for |- ; A C = ; A C with typecode |-
8 3 nn0cni C
9 2 nn0cni B
10 8 9 addcomi C + B = B + C
11 1 3 2 7 10 decaddi Could not format ( ; A C + B ) = ; A ( B + C ) : No typesetting found for |- ( ; A C + B ) = ; A ( B + C ) with typecode |-
12 6 11 eqtr4i Could not format ( ; A B + C ) = ( ; A C + B ) : No typesetting found for |- ( ; A B + C ) = ( ; A C + B ) with typecode |-