Metamath Proof Explorer

Theorem naddassd

Description: Natural addition associates. Deduction form. (Contributed by Scott Fenton, 30-Jul-2026)

Ref Expression
Hypotheses nadd.1 ⊢ φ → A ∈ On
nadd.2 ⊢ φ → B ∈ On
nadd.3 ⊢ φ → C ∈ On
Assertion naddassd ⊢ φ → A + B + C = A + B + C

Proof

Step Hyp Ref Expression
1 nadd.1 ⊢ φ → A ∈ On
2 nadd.2 ⊢ φ → B ∈ On
3 nadd.3 ⊢ φ → C ∈ On
4 naddass ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B + C = A + B + C
5 1 2 3 4 syl3anc ⊢ φ → A + B + C = A + B + C