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 e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( A +no B ) +no ( C +no D ) ) = ( ( A +no C ) +no ( D +no B ) ) )

Proof

Step Hyp Ref Expression
1 nadd4 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( A +no B ) +no ( C +no D ) ) = ( ( A +no C ) +no ( B +no D ) ) )
2 naddcom 
 |-  ( ( B e. On /\ D e. On ) -> ( B +no D ) = ( D +no B ) )
3 2 ad2ant2l 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( B +no D ) = ( D +no B ) )
4 3 oveq2d 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( A +no C ) +no ( B +no D ) ) = ( ( A +no C ) +no ( D +no B ) ) )
5 1 4 eqtrd 
 |-  ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( A +no B ) +no ( C +no D ) ) = ( ( A +no C ) +no ( D +no B ) ) )