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 318 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
31, 2bitr3di 289 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
43necon4abid 2981 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209   = wceq 1543  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 210  df-ne 2941
This theorem is referenced by:  necon4bid  2986  omwordi  8299  omass  8308  nnmwordi  8363  sdom1  8878  pceq0  16424  f1otrspeq  18839  pmtrfinv  18853  symggen  18862  psgnunilem1  18885  mdetralt  21505  mdetunilem7  21515  ftalem5  25959  fsumvma  26094  dchrelbas4  26124  fvdifsupp  30738  creq0  30790  fsumcvg4  31614  nosepssdm  33626  lkreqN  36921  flt4lem5elem  40191
  Copyright terms: Public domain W3C validator