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 ⊢ 𝐴 ∈ ℕ
nnaddcomli.2 ⊢ 𝐵 ∈ ℕ
nnaddcomli.3 ⊢ ( 𝐴 + 𝐵 ) = 𝐶
Assertion nnaddcomli ( 𝐵 + 𝐴 ) = 𝐶

Proof

Step Hyp Ref Expression
1 nnaddcomli.1 ⊢ 𝐴 ∈ ℕ
2 nnaddcomli.2 ⊢ 𝐵 ∈ ℕ
3 nnaddcomli.3 ⊢ ( 𝐴 + 𝐵 ) = 𝐶
4 nnaddcom ⊢ ( ( 𝐵 ∈ ℕ ∧ 𝐴 ∈ ℕ ) → ( 𝐵 + 𝐴 ) = ( 𝐴 + 𝐵 ) )
5 2 1 4 mp2an ⊢ ( 𝐵 + 𝐴 ) = ( 𝐴 + 𝐵 )
6 5 3 eqtri ⊢ ( 𝐵 + 𝐴 ) = 𝐶