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

Theorem necon2bbid 2825
 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 303 . . 3 (𝜓 ↔ ¬ ¬ 𝜓)
2 necon2bbid.1 . . 3 (𝜑 → (𝜓𝐴𝐵))
31, 2syl5rbbr 274 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ ¬ 𝜓))
43necon4abid 2822 1 (𝜑 → (𝐴 = 𝐵 ↔ ¬ 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780 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 196  df-ne 2782 This theorem is referenced by:  necon4bid  2827  omwordi  7538  omass  7547  nnmwordi  7602  sdom1  8045  pceq0  15413  f1otrspeq  17690  pmtrfinv  17704  symggen  17713  psgnunilem1  17736  mdetralt  20233  mdetunilem7  20243  ftalem5  24603  fsumvma  24738  dchrelbas4  24768  fsumcvg4  29324  lkreqN  33475
 Copyright terms: Public domain W3C validator