Metamath Proof Explorer

Theorem subsub23

Description: Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢B∈ℂ∧C∈ℂ→B+C=C+B
2 1 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+C=C+B
3 2 eqeq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+C=A↔C+B=A
4 subadd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B=C↔B+C=A
5 subadd ⊢A∈ℂ∧C∈ℂ∧B∈ℂ→A−C=B↔C+B=A
6 5 3com23 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−C=B↔C+B=A
7 3 4 6 3bitr4d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B=C↔A−C=B