Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  addsub Structured version   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 ((A B 𝐶 ℂ) → ((A + B) − 𝐶) = ((A𝐶) + B))

StepHypRef Expression
1 addcom 6927 . . . 4 ((A B ℂ) → (A + B) = (B + A))
21oveq1d 5470 . . 3 ((A B ℂ) → ((A + B) − 𝐶) = ((B + A) − 𝐶))
323adant3 923 . 2 ((A B 𝐶 ℂ) → ((A + B) − 𝐶) = ((B + A) − 𝐶))
4 addsubass 6998 . . 3 ((B A 𝐶 ℂ) → ((B + A) − 𝐶) = (B + (A𝐶)))
543com12 1107 . 2 ((A B 𝐶 ℂ) → ((B + A) − 𝐶) = (B + (A𝐶)))
6 subcl 6987 . . . . 5 ((A 𝐶 ℂ) → (A𝐶) ℂ)
7 addcom 6927 . . . . 5 ((B (A𝐶) ℂ) → (B + (A𝐶)) = ((A𝐶) + B))
86, 7sylan2 270 . . . 4 ((B (A 𝐶 ℂ)) → (B + (A𝐶)) = ((A𝐶) + B))
983impb 1099 . . 3 ((B A 𝐶 ℂ) → (B + (A𝐶)) = ((A𝐶) + B))
1093com12 1107 . 2 ((A B 𝐶 ℂ) → (B + (A𝐶)) = ((A𝐶) + B))
113, 5, 103eqtrd 2073 1 ((A B 𝐶 ℂ) → ((A + B) − 𝐶) = ((A𝐶) + B))