This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( 𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ ) ) → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) − 𝐷 ) = ( ( ( 𝐴 + 𝐶 ) − 𝐷 ) + 𝐵 ) )