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

Theorem necon2bbid 2824
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 notnotb 302 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
2 necon2bbid.1 . . 3 (𝜑 → (𝜓𝐴𝐵))
31, 2syl5rbbr 273 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
43necon4abid 2821 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194   = wceq 1474  wne 2779
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 195  df-ne 2781
This theorem is referenced by:  necon4bid  2826  omwordi  7515  omass  7524  nnmwordi  7579  sdom1  8022  pceq0  15359  f1otrspeq  17636  pmtrfinv  17650  symggen  17659  psgnunilem1  17682  mdetralt  20175  mdetunilem7  20185  ftalem5  24520  fsumvma  24655  dchrelbas4  24685  fsumcvg4  29130  lkreqN  33278
  Copyright terms: Public domain W3C validator