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

Theorem necon1ad 2949
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 2945 . 2 (𝜑 → (𝐴𝐵 → ¬ ¬ 𝜓))
3 notnotr 125 . 2 (¬ ¬ 𝜓𝜓)
42, 3syl6 35 1 (𝜑 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1632  wne 2932
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 197  df-ne 2933
This theorem is referenced by:  prnebg  4533  fr0  5245  sofld  5739  onmindif2  7178  suppss  7495  suppss2  7499  uniinqs  7996  dfac5lem4  9159  uzwo  11964  seqf1olem1  13054  seqf1olem2  13055  hashnncl  13369  pceq0  15797  vdwmc2  15905  odcau  18239  islss  19157  fidomndrnglem  19528  mvrf1  19647  mpfrcl  19740  obs2ss  20295  obslbs  20296  dsmmacl  20307  regr1lem2  21765  iccpnfhmeo  22965  itg10a  23696  dvlip  23975  deg1ge  24077  elply2  24171  coeeulem  24199  dgrle  24218  coemullem  24225  basellem2  25028  perfectlem2  25175  lgsabs1  25281  lnon0  27983  atsseq  29536  disjif2  29722  cvmseu  31586  nosepon  32145  noextenddif  32148  matunitlindf  33738  poimirlem2  33742  poimirlem18  33758  poimirlem21  33761  itg2addnclem  33792  lsatcmp  34811  lsatcmp2  34812  ltrnnid  35943  trlatn0  35980  cdlemh  36625  dochlkr  37194  perfectALTVlem2  42159
  Copyright terms: Public domain W3C validator