Theorem necon1ad 2973

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

Step	Hyp	Ref	Expression
1		necon1ad.1	. . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))
2	1	necon3ad 2969	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ ¬ 𝜓))
3		notnotr 130	. 2 ⊢ (¬ ¬ 𝜓 → 𝜓)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 2957

This theorem is referenced by:  prnebg  4813  fr0  5623  sofld  6169  onmindif2  7786  suppss  8169  suppss2  8175  uniinqs  8774  dfac5lem4  10079  dfac5lem4OLD  10081  uzwo  12909  seqf1olem1  14051  seqf1olem2  14052  hashnncl  14376  pceq0  16890  vdwmc2  16998  odcau  19627  fidomndrnglem  20801  islss  20981  obs2ss  21761  obslbs  21762  dsmmacl  21773  mvrf1  22017  mpfrcl  22118  mhpvarcl  22193  regr1lem2  23780  iccpnfhmeo  24987  itg10a  25752  dvlip  26035  deg1ge  26138  elply2  26236  coeeulem  26264  dgrle  26283  coemullem  26290  basellem2  27123  perfectlem2  27271  lgsabs1  27377  nosepon  27706  noextenddif  27709  lnon0  30947  atsseq  32496  disjif2  32730  prmidl0  33598  cvmseu  35590  matunitlindf  38081  poimirlem2  38085  poimirlem18  38101  poimirlem21  38104  itg2addnclem  38134  lsatcmp  39591  lsatcmp2  39592  ltrnnid  40724  trlatn0  40760  cdlemh  41405  dochlkr  41973  perfectALTVlem2  48308