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