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

Theorem necon2bbid 2984
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 315 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
31, 2bitr3di 286 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
43necon4abid 2981 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1542  wne 2940
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 2941
This theorem is referenced by:  necon4bid  2986  omwordi  8519  omass  8528  nnmwordi  8583  sdom1OLD  9190  pceq0  16748  f1otrspeq  19234  pmtrfinv  19248  symggen  19257  psgnunilem1  19280  mdetralt  21973  mdetunilem7  21983  ftalem5  26442  fsumvma  26577  dchrelbas4  26607  nosepssdm  27050  fvdifsupp  31645  creq0  31699  fsumcvg4  32588  lkreqN  37678  flt4lem5elem  41032
  Copyright terms: Public domain W3C validator