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

Theorem necon2bbid 3030
 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 3027 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1538   ≠ wne 2987 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 2988 This theorem is referenced by:  necon4bid  3032  omwordi  8183  omass  8192  nnmwordi  8247  sdom1  8705  pceq0  16200  f1otrspeq  18571  pmtrfinv  18585  symggen  18594  psgnunilem1  18617  mdetralt  21223  mdetunilem7  21233  ftalem5  25672  fsumvma  25807  dchrelbas4  25837  fvdifsupp  30454  creq0  30507  fsumcvg4  31318  nosepssdm  33318  lkreqN  36485
 Copyright terms: Public domain W3C validator