Theorem nadd42

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

	Ref	Expression
Assertion	nadd42	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 ( D +no B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nadd4	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 |-
2		naddcom	Could not format ( ( B e. On /\ D e. On ) -> ( B +no D ) = ( D +no B ) ) : No typesetting found for |- ( ( B e. On /\ D e. On ) -> ( B +no D ) = ( D +no B ) ) with typecode |-
3	2	ad2ant2l	Could not format ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( B +no D ) = ( D +no B ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( C e. On /\ D e. On ) ) -> ( B +no D ) = ( D +no B ) ) with typecode |-
4	3	oveq2d	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 ( D +no B ) ) ) : 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 ( D +no B ) ) ) with typecode |-
5	1 4	eqtrd	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 ( D +no B ) ) ) : 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 ( D +no B ) ) ) with typecode |-