Metamath Proof Explorer

Theorem negcon2

Description: Negative contraposition law. (Contributed by NM, 14-Nov-2004)

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

Proof

Step Hyp Ref Expression
1 eqcom ⊢ A = − B ↔ − B = A
2 negcon1 ⊢ A ∈ ℂ ∧ B ∈ ℂ → − A = B ↔ − B = A
3 1 2 bitr4id ⊢ A ∈ ℂ ∧ B ∈ ℂ → A = − B ↔ − A = B
4 eqcom ⊢ − A = B ↔ B = − A
5 3 4 bitrdi ⊢ A ∈ ℂ ∧ B ∈ ℂ → A = − B ↔ B = − A