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

Theorem necon2bbid 2983
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 necon2bbid.1 . . 3 (𝜑 → (𝜓𝐴𝐵))
2 notnotb 314 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
31, 2bitr3di 285 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
43necon4abid 2980 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1541  wne 2939
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 206  df-ne 2940
This theorem is referenced by:  necon4bid  2985  omwordi  8554  omass  8563  nnmwordi  8618  sdom1OLD  9226  pceq0  16786  f1otrspeq  19279  pmtrfinv  19293  symggen  19302  psgnunilem1  19325  mdetralt  22039  mdetunilem7  22049  ftalem5  26508  fsumvma  26643  dchrelbas4  26673  nosepssdm  27116  fvdifsupp  31777  creq0  31831  fsumcvg4  32761  lkreqN  37845  flt4lem5elem  41175
  Copyright terms: Public domain W3C validator