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

Theorem necon1ad 2988
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 2984 . 2 (𝜑 → (𝐴𝐵 → ¬ ¬ 𝜓))
3 notnotr 128 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1653  wne 2971
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 199  df-ne 2972
This theorem is referenced by:  prnebg  4574  fr0  5291  sofld  5798  onmindif2  7246  suppss  7563  suppss2  7567  uniinqs  8065  dfac5lem4  9235  uzwo  11996  seqf1olem1  13094  seqf1olem2  13095  hashnncl  13407  pceq0  15908  vdwmc2  16016  odcau  18332  islss  19253  fidomndrnglem  19629  mvrf1  19748  mpfrcl  19840  obs2ss  20398  obslbs  20399  dsmmacl  20410  regr1lem2  21872  iccpnfhmeo  23072  itg10a  23818  dvlip  24097  deg1ge  24199  elply2  24293  coeeulem  24321  dgrle  24340  coemullem  24347  basellem2  25160  perfectlem2  25307  lgsabs1  25413  lnon0  28178  atsseq  29731  disjif2  29911  cvmseu  31775  nosepon  32331  noextenddif  32334  matunitlindf  33896  poimirlem2  33900  poimirlem18  33916  poimirlem21  33919  itg2addnclem  33949  lsatcmp  35024  lsatcmp2  35025  ltrnnid  36157  trlatn0  36193  cdlemh  36838  dochlkr  37406  perfectALTVlem2  42413
  Copyright terms: Public domain W3C validator