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

Theorem necon2bbid 2982
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 2979 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206   = wceq 1537  wne 2938
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 207  df-ne 2939
This theorem is referenced by:  necon4bid  2984  fvdifsupp  8195  omwordi  8608  omass  8617  nnmwordi  8672  sdom1OLD  9277  pceq0  16905  f1otrspeq  19480  pmtrfinv  19494  symggen  19503  psgnunilem1  19526  mdetralt  22630  mdetunilem7  22640  ftalem5  27135  fsumvma  27272  dchrelbas4  27302  nosepssdm  27746  creq0  32753  fsumcvg4  33911  lkreqN  39152  flt4lem5elem  42638
  Copyright terms: Public domain W3C validator