Theorem 2addsub

Description: Law for subtraction and addition. (Contributed by NM, 20-Nov-2005)

	Ref	Expression
Assertion	2addsub	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) − 𝐷 ) = ( ( ( 𝐴 + 𝐶 ) − 𝐷 ) + 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		add32	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( ( 𝐴 + 𝐶 ) + 𝐵 ) )
2	1	3expa	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( ( 𝐴 + 𝐶 ) + 𝐵 ) )
3	2	adantrr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( 𝐴 + 𝐵 ) + 𝐶 ) = ( ( 𝐴 + 𝐶 ) + 𝐵 ) )
4	3	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) − 𝐷 ) = ( ( ( 𝐴 + 𝐶 ) + 𝐵 ) − 𝐷 ) )
5		addcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + 𝐶 ) ∈ ℂ )
6		addsub	⊢ ( ( ( 𝐴 + 𝐶 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( ( ( 𝐴 + 𝐶 ) + 𝐵 ) − 𝐷 ) = ( ( ( 𝐴 + 𝐶 ) − 𝐷 ) + 𝐵 ) )
7	6	3expb	⊢ ( ( ( 𝐴 + 𝐶 ) ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐶 ) + 𝐵 ) − 𝐷 ) = ( ( ( 𝐴 + 𝐶 ) − 𝐷 ) + 𝐵 ) )
8	5 7	sylan	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐶 ) + 𝐵 ) − 𝐷 ) = ( ( ( 𝐴 + 𝐶 ) − 𝐷 ) + 𝐵 ) )
9	8	an4s	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐶 ) + 𝐵 ) − 𝐷 ) = ( ( ( 𝐴 + 𝐶 ) − 𝐷 ) + 𝐵 ) )
10	4 9	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) − 𝐷 ) = ( ( ( 𝐴 + 𝐶 ) − 𝐷 ) + 𝐵 ) )