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

Metamath Proof Explorer

Theorem nnaddcomli

Description: Version of addcomli for natural numbers. (Contributed by Steven Nguyen, 1-Aug-2023)

Ref Expression
Hypotheses nnaddcomli.1 ⊢ A ∈ ℕ
nnaddcomli.2 ⊢ B ∈ ℕ
nnaddcomli.3 ⊢ A + B = C
Assertion nnaddcomli ⊢ B + A = C

Proof

Step Hyp Ref Expression
1 nnaddcomli.1 ⊢ A ∈ ℕ
2 nnaddcomli.2 ⊢ B ∈ ℕ
3 nnaddcomli.3 ⊢ A + B = C
4 nnaddcom ⊢ B ∈ ℕ ∧ A ∈ ℕ → B + A = A + B
5 2 1 4 mp2an ⊢ B + A = A + B
6 5 3 eqtri ⊢ B + A = C