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

Theorem necon1ad 2957
Description: Contrapositive deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
necon1ad.1 (𝜑 → (¬ 𝜓𝐴 = 𝐵))
Assertion
Ref Expression
necon1ad (𝜑 → (𝐴𝐵𝜓))

Proof of Theorem necon1ad
StepHypRef Expression
1 necon1ad.1 . . 3 (𝜑 → (¬ 𝜓𝐴 = 𝐵))
21necon3ad 2953 . 2 (𝜑 → (𝐴𝐵 → ¬ ¬ 𝜓))
3 notnotr 130 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1540  wne 2940
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 2941
This theorem is referenced by:  prnebg  4856  fr0  5663  sofld  6207  onmindif2  7827  suppss  8219  suppss2  8225  uniinqs  8837  dfac5lem4  10166  dfac5lem4OLD  10168  uzwo  12953  seqf1olem1  14082  seqf1olem2  14083  hashnncl  14405  pceq0  16909  vdwmc2  17017  odcau  19622  fidomndrnglem  20773  islss  20932  obs2ss  21749  obslbs  21750  dsmmacl  21761  mvrf1  22006  mpfrcl  22109  mhpvarcl  22152  regr1lem2  23748  iccpnfhmeo  24976  itg10a  25745  dvlip  26032  deg1ge  26137  elply2  26235  coeeulem  26263  dgrle  26282  coemullem  26289  basellem2  27125  perfectlem2  27274  lgsabs1  27380  nosepon  27710  noextenddif  27713  lnon0  30817  atsseq  32366  disjif2  32594  prmidl0  33478  cvmseu  35281  matunitlindf  37625  poimirlem2  37629  poimirlem18  37645  poimirlem21  37648  itg2addnclem  37678  lsatcmp  39004  lsatcmp2  39005  ltrnnid  40138  trlatn0  40174  cdlemh  40819  dochlkr  41387  perfectALTVlem2  47709
  Copyright terms: Public domain W3C validator