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

Theorem necon2bbid 2963
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 304 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
2 necon2bbid.1 . . 3 (𝜑 → (𝜓𝐴𝐵))
31, 2syl5rbbr 275 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
43necon4abid 2960 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196   = wceq 1620  wne 2920
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 197  df-ne 2921
This theorem is referenced by:  necon4bid  2965  omwordi  7808  omass  7817  nnmwordi  7872  sdom1  8313  pceq0  15748  f1otrspeq  18038  pmtrfinv  18052  symggen  18061  psgnunilem1  18084  mdetralt  20587  mdetunilem7  20597  ftalem5  24973  fsumvma  25108  dchrelbas4  25138  fsumcvg4  30276  nosepssdm  32113  lkreqN  34929
  Copyright terms: Public domain W3C validator