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 1533  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 209  df-ne 3017
This theorem is referenced by:  prnebg  4785  fr0  5533  sofld  6043  onmindif2  7526  suppss  7859  suppss2  7863  uniinqs  8376  dfac5lem4  9551  uzwo  12310  seqf1olem1  13408  seqf1olem2  13409  hashnncl  13726  pceq0  16206  vdwmc2  16314  odcau  18728  islss  19705  fidomndrnglem  20078  mvrf1  20204  mpfrcl  20297  obs2ss  20872  obslbs  20873  dsmmacl  20884  regr1lem2  22347  iccpnfhmeo  23548  itg10a  24310  dvlip  24589  deg1ge  24691  elply2  24785  coeeulem  24813  dgrle  24832  coemullem  24839  basellem2  25658  perfectlem2  25805  lgsabs1  25911  lnon0  28574  atsseq  30123  disjif2  30330  cvmseu  32523  nosepon  33172  noextenddif  33175  matunitlindf  34889  poimirlem2  34893  poimirlem18  34909  poimirlem21  34912  itg2addnclem  34942  lsatcmp  36138  lsatcmp2  36139  ltrnnid  37271  trlatn0  37307  cdlemh  37952  dochlkr  38520  perfectALTVlem2  43888
  Copyright terms: Public domain W3C validator