Theorem nadd4

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

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

Proof

Step	Hyp	Ref	Expression
1		nadd32	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 +no 𝐵 ) +no 𝐶 ) = ( ( 𝐴 +no 𝐶 ) +no 𝐵 ) )
2	1	3expa	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐶 ∈ On ) → ( ( 𝐴 +no 𝐵 ) +no 𝐶 ) = ( ( 𝐴 +no 𝐶 ) +no 𝐵 ) )
3	2	adantrr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 +no 𝐵 ) +no 𝐶 ) = ( ( 𝐴 +no 𝐶 ) +no 𝐵 ) )
4	3	oveq1d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( ( 𝐴 +no 𝐵 ) +no 𝐶 ) +no 𝐷 ) = ( ( ( 𝐴 +no 𝐶 ) +no 𝐵 ) +no 𝐷 ) )
5		naddcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +no 𝐵 ) ∈ On )
6	5	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 +no 𝐵 ) ∈ On )
7		simprl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐶 ∈ On )
8		simprr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐷 ∈ On )
9		naddass	⊢ ( ( ( 𝐴 +no 𝐵 ) ∈ On ∧ 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( ( ( 𝐴 +no 𝐵 ) +no 𝐶 ) +no 𝐷 ) = ( ( 𝐴 +no 𝐵 ) +no ( 𝐶 +no 𝐷 ) ) )
10	6 7 8 9	syl3anc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( ( 𝐴 +no 𝐵 ) +no 𝐶 ) +no 𝐷 ) = ( ( 𝐴 +no 𝐵 ) +no ( 𝐶 +no 𝐷 ) ) )
11		naddcl	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 +no 𝐶 ) ∈ On )
12	11	ad2ant2r	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( 𝐴 +no 𝐶 ) ∈ On )
13		simplr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → 𝐵 ∈ On )
14		naddass	⊢ ( ( ( 𝐴 +no 𝐶 ) ∈ On ∧ 𝐵 ∈ On ∧ 𝐷 ∈ On ) → ( ( ( 𝐴 +no 𝐶 ) +no 𝐵 ) +no 𝐷 ) = ( ( 𝐴 +no 𝐶 ) +no ( 𝐵 +no 𝐷 ) ) )
15	12 13 8 14	syl3anc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( ( 𝐴 +no 𝐶 ) +no 𝐵 ) +no 𝐷 ) = ( ( 𝐴 +no 𝐶 ) +no ( 𝐵 +no 𝐷 ) ) )
16	4 10 15	3eqtr3d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) ) → ( ( 𝐴 +no 𝐵 ) +no ( 𝐶 +no 𝐷 ) ) = ( ( 𝐴 +no 𝐶 ) +no ( 𝐵 +no 𝐷 ) ) )