Theorem nadd4

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

	Ref	Expression
Assertion	nadd4	Could not format assertion : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nadd32	Could not format ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) : No typesetting found for |- ( ( A e. On /\ B e. On /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) with typecode |-
2	1	3expa	Could not format ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) with typecode |-
3	2	adantrr	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( A +no B ) +no C ) = ( ( A +no C ) +no B ) ) with typecode |-
4	3	oveq1d	Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
5		naddcl	Could not format ( ( A e. On /\ B e. On ) -> ( A +no B ) e. On ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( A +no B ) e. On ) with typecode |-
6	5	adantr	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( A +no B ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( A +no B ) e. On ) with typecode |-
7		simprl	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to C\in \mathrm{On}$$
8		simprr	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to D\in \mathrm{On}$$
9		naddass	Could not format ( ( ( A +no B ) e. On /\ C e. On /\ D e. On ) -> ( ( ( A +no B ) +no C ) +no D ) = ( ( A +no B ) +no ( C +no D ) ) ) : No typesetting found for |- ( ( ( A +no B ) e. On /\ C e. On /\ D e. On ) -> ( ( ( A +no B ) +no C ) +no D ) = ( ( A +no B ) +no ( C +no D ) ) ) with typecode |-
10	6 7 8 9	syl3anc	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( A +no B ) +no C ) +no D ) = ( ( A +no B ) +no ( C +no D ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( A +no B ) +no C ) +no D ) = ( ( A +no B ) +no ( C +no D ) ) ) with typecode |-
11		naddcl	Could not format ( ( A e. On /\ C e. On ) -> ( A +no C ) e. On ) : No typesetting found for |- ( ( A e. On /\ C e. On ) -> ( A +no C ) e. On ) with typecode |-
12	11	ad2ant2r	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( A +no C ) e. On ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( A +no C ) e. On ) with typecode |-
13		simplr	$$⊢\left(\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\wedge \left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\right)\to B\in \mathrm{On}$$
14		naddass	Could not format ( ( ( A +no C ) e. On /\ B e. On /\ D e. On ) -> ( ( ( A +no C ) +no B ) +no D ) = ( ( A +no C ) +no ( B +no D ) ) ) : No typesetting found for |- ( ( ( A +no C ) e. On /\ B e. On /\ D e. On ) -> ( ( ( A +no C ) +no B ) +no D ) = ( ( A +no C ) +no ( B +no D ) ) ) with typecode |-
15	12 13 8 14	syl3anc	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( A +no C ) +no B ) +no D ) = ( ( A +no C ) +no ( B +no D ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( ( ( A +no C ) +no B ) +no D ) = ( ( A +no C ) +no ( B +no D ) ) ) with typecode |-
16	4 10 15	3eqtr3d	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-