Metamath Proof Explorer

Theorem nadd42

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

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

Proof

Step Hyp Ref Expression
1 nadd4 ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + B + C + D = A + C + B + D
2 naddcom ⊢ B ∈ On ∧ D ∈ On → B + D = D + B
3 2 ad2ant2l ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → B + D = D + B
4 3 oveq2d ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + C + B + D = A + C + D + B
5 1 4 eqtrd ⊢ A ∈ On ∧ B ∈ On ∧ C ∈ On ∧ D ∈ On → A + B + C + D = A + C + D + B