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

Theorem necon1ad 3033
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 3029 . 2 (𝜑 → (𝐴𝐵 → ¬ ¬ 𝜓))
3 notnotr 132 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  prnebg  4780  fr0  5528  sofld  6038  onmindif2  7515  suppss  7851  suppss2  7855  uniinqs  8367  dfac5lem4  9541  uzwo  12300  seqf1olem1  13399  seqf1olem2  13400  hashnncl  13717  pceq0  16197  vdwmc2  16305  odcau  18660  islss  19637  fidomndrnglem  20009  mvrf1  20135  mpfrcl  20228  obs2ss  20803  obslbs  20804  dsmmacl  20815  regr1lem2  22278  iccpnfhmeo  23478  itg10a  24240  dvlip  24519  deg1ge  24621  elply2  24715  coeeulem  24743  dgrle  24762  coemullem  24769  basellem2  25587  perfectlem2  25734  lgsabs1  25840  lnon0  28503  atsseq  30052  disjif2  30260  cvmseu  32421  nosepon  33070  noextenddif  33073  matunitlindf  34772  poimirlem2  34776  poimirlem18  34792  poimirlem21  34795  itg2addnclem  34825  lsatcmp  36021  lsatcmp2  36022  ltrnnid  37154  trlatn0  37190  cdlemh  37835  dochlkr  38403  perfectALTVlem2  43734
  Copyright terms: Public domain W3C validator