Metamath Proof Explorer

Theorem nadd4

Description: Rearragement of terms in a quadruple sum. (Contributed by Scott Fenton, 5-Feb-2025)

Ref Expression
Assertion nadd4 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + B + C + D = A + C + B + D

Proof

Step Hyp Ref Expression
1 nadd32 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B + C = A + C + B
2 1 3expa ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On → A + B + C = A + C + B
3 2 adantrr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + B + C = A + C + B
4 3 oveq1d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + B + C + D = A + C + B + D
5 naddcl ⊢ A ∈ On ∧ B ∈ On → A + B ∈ On
6 5 adantr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + B ∈ On
7 simprl ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → C ∈ On
8 simprr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → D ∈ On
9 naddass ⊢ A + B ∈ On ∧ C ∈ On ∧ D ∈ On → A + B + C + D = A + B + C + D
10 6 7 8 9 syl3anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + B + C + D = A + B + C + D
11 naddcl ⊢ A ∈ On ∧ C ∈ On → A + C ∈ On
12 11 ad2ant2r ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + C ∈ On
13 simplr ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → B ∈ On
14 naddass ⊢ A + C ∈ On ∧ B ∈ On ∧ D ∈ On → A + C + B + D = A + C + B + D
15 12 13 8 14 syl3anc ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + C + B + D = A + C + B + D
16 4 10 15 3eqtr3d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + B + C + D = A + C + B + D