Theorem addsub12

Description: Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005)

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

Proof

Step	Hyp	Ref	Expression
1		subadd23	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) + 𝐵 ) = ( 𝐴 + ( 𝐵 − 𝐶 ) ) )
2		subcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 − 𝐶 ) ∈ ℂ )
3		addcom	⊢ ( ( ( 𝐴 − 𝐶 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) + 𝐵 ) = ( 𝐵 + ( 𝐴 − 𝐶 ) ) )
4	2 3	stoic3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 − 𝐶 ) + 𝐵 ) = ( 𝐵 + ( 𝐴 − 𝐶 ) ) )
5	1 4	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + ( 𝐵 − 𝐶 ) ) = ( 𝐵 + ( 𝐴 − 𝐶 ) ) )
6	5	3com23	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 + ( 𝐵 − 𝐶 ) ) = ( 𝐵 + ( 𝐴 − 𝐶 ) ) )