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

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 |-