Theorem nadd42

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

	Ref	Expression
Assertion	nadd42	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 +no 𝐵 ) +no ( 𝐶 +no 𝐷 ) ) = ( ( 𝐴 +no 𝐶 ) +no ( 𝐷 +no 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nadd4	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 +no 𝐵 ) +no ( 𝐶 +no 𝐷 ) ) = ( ( 𝐴 +no 𝐶 ) +no ( 𝐵 +no 𝐷 ) ) )
2		naddcom	⊢ ( ( 𝐵 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐵 +no 𝐷 ) = ( 𝐷 +no 𝐵 ) )
3	2	ad2ant2l	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐵 +no 𝐷 ) = ( 𝐷 +no 𝐵 ) )
4	3	oveq2d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 +no 𝐶 ) +no ( 𝐵 +no 𝐷 ) ) = ( ( 𝐴 +no 𝐶 ) +no ( 𝐷 +no 𝐵 ) ) )
5	1 4	eqtrd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 +no 𝐵 ) +no ( 𝐶 +no 𝐷 ) ) = ( ( 𝐴 +no 𝐶 ) +no ( 𝐷 +no 𝐵 ) ) )