Metamath Proof Explorer

Theorem sub31

Description: Swap the first and third terms in a double subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion sub31 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B−C=C−B−A

Proof

Step Hyp Ref Expression
1 simp1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A∈ℂ
2 simpr ⊢B∈ℂ∧C∈ℂ→C∈ℂ
3 simpl ⊢B∈ℂ∧C∈ℂ→B∈ℂ
4 2 3 subcld ⊢B∈ℂ∧C∈ℂ→C−B∈ℂ
5 4 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C−B∈ℂ
6 1 5 addcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+C-B=C-B+A
7 subsub2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B−C=A+C-B
8 simp3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C∈ℂ
9 simp2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B∈ℂ
10 8 9 1 subsubd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C−B−A=C-B+A
11 6 7 10 3eqtr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B−C=C−B−A