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 1542  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 206  df-ne 2941
This theorem is referenced by:  prnebg  4817  fr0  5616  sofld  6143  onmindif2  7746  suppss  8129  suppssOLD  8130  suppss2  8135  uniinqs  8742  dfac5lem4  10070  uzwo  12844  seqf1olem1  13956  seqf1olem2  13957  hashnncl  14275  pceq0  16751  vdwmc2  16859  odcau  19394  islss  20439  fidomndrnglem  20800  obs2ss  21158  obslbs  21159  dsmmacl  21170  mvrf1  21417  mpfrcl  21518  mhpvarcl  21561  regr1lem2  23114  iccpnfhmeo  24331  itg10a  25098  dvlip  25380  deg1ge  25486  elply2  25580  coeeulem  25608  dgrle  25627  coemullem  25634  basellem2  26454  perfectlem2  26601  lgsabs1  26707  nosepon  27036  noextenddif  27039  lnon0  29789  atsseq  31338  disjif2  31552  prmidl0  32278  cvmseu  33934  matunitlindf  36126  poimirlem2  36130  poimirlem18  36146  poimirlem21  36149  itg2addnclem  36179  lsatcmp  37515  lsatcmp2  37516  ltrnnid  38649  trlatn0  38685  cdlemh  39330  dochlkr  39898  perfectALTVlem2  46004
  Copyright terms: Public domain W3C validator