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