MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon2bbid Structured version   Visualization version   GIF version

Theorem necon2bbid 3059
Description: Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
Hypothesis
Ref Expression
necon2bbid.1 (𝜑 → (𝜓𝐴𝐵))
Assertion
Ref Expression
necon2bbid (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))

Proof of Theorem necon2bbid
StepHypRef Expression
1 notnotb 316 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
2 necon2bbid.1 . . 3 (𝜑 → (𝜓𝐴𝐵))
31, 2syl5rbbr 287 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
43necon4abid 3056 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208  df-ne 3017
This theorem is referenced by:  necon4bid  3061  omwordi  8187  omass  8196  nnmwordi  8251  sdom1  8707  pceq0  16197  f1otrspeq  18506  pmtrfinv  18520  symggen  18529  psgnunilem1  18552  mdetralt  21147  mdetunilem7  21157  ftalem5  25582  fsumvma  25717  dchrelbas4  25747  creq0  30398  fsumcvg4  31093  nosepssdm  33088  lkreqN  36188
  Copyright terms: Public domain W3C validator