Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  addsub GIF version

 Description: Law for addition and subtraction. (Contributed by NM, 19-Aug-2001.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
addsub ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴𝐶) + 𝐵))

Proof of Theorem addsub
StepHypRef Expression
1 addcom 7716 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
21oveq1d 5705 . . 3 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐵 + 𝐴) − 𝐶))
323adant3 966 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐵 + 𝐴) − 𝐶))
4 addsubass 7789 . . 3 ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐵 + 𝐴) − 𝐶) = (𝐵 + (𝐴𝐶)))
543com12 1150 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐵 + 𝐴) − 𝐶) = (𝐵 + (𝐴𝐶)))
6 subcl 7778 . . . . 5 ((𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐶) ∈ ℂ)
7 addcom 7716 . . . . 5 ((𝐵 ∈ ℂ ∧ (𝐴𝐶) ∈ ℂ) → (𝐵 + (𝐴𝐶)) = ((𝐴𝐶) + 𝐵))
86, 7sylan2 281 . . . 4 ((𝐵 ∈ ℂ ∧ (𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ)) → (𝐵 + (𝐴𝐶)) = ((𝐴𝐶) + 𝐵))
983impb 1142 . . 3 ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵 + (𝐴𝐶)) = ((𝐴𝐶) + 𝐵))
1093com12 1150 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐵 + (𝐴𝐶)) = ((𝐴𝐶) + 𝐵))
113, 5, 103eqtrd 2131 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) − 𝐶) = ((𝐴𝐶) + 𝐵))