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 315 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
31, 2bitr3di 286 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
43necon4abid 2980 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206   = wceq 1539  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 207  df-ne 2940
This theorem is referenced by:  necon4bid  2985  fvdifsupp  8197  omwordi  8610  omass  8619  nnmwordi  8674  sdom1OLD  9280  pceq0  16910  f1otrspeq  19466  pmtrfinv  19480  symggen  19489  psgnunilem1  19512  mdetralt  22615  mdetunilem7  22625  ftalem5  27121  fsumvma  27258  dchrelbas4  27288  nosepssdm  27732  creq0  32747  fsumcvg4  33950  lkreqN  39172  flt4lem5elem  42666
  Copyright terms: Public domain W3C validator