Metamath Proof Explorer

Theorem negcon1

Description: Negative contraposition law. (Contributed by NM, 9-May-2004)

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

Proof

Step Hyp Ref Expression
1 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
2 neg11 ⊢ − A ∈ ℂ ∧ B ∈ ℂ → − − A = − B ↔ − A = B
3 1 2 sylan ⊢ A ∈ ℂ ∧ B ∈ ℂ → − − A = − B ↔ − A = B
4 negneg ⊢ A ∈ ℂ → − − A = A
5 4 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ → − − A = A
6 5 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → − − A = − B ↔ A = − B
7 3 6 bitr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A = B ↔ A = − B
8 eqcom ⊢ A = − B ↔ − B = A
9 7 8 bitrdi ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A = B ↔ − B = A