Theorem necon1ad 2942

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 2938	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ ¬ 𝜓))
3		notnotr 130	. 2 ⊢ (¬ ¬ 𝜓 → 𝜓)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  prnebg  4820  fr0  5616  sofld  6160  onmindif2  7783  suppss  8173  suppss2  8179  uniinqs  8770  dfac5lem4  10079  dfac5lem4OLD  10081  uzwo  12870  seqf1olem1  14006  seqf1olem2  14007  hashnncl  14331  pceq0  16842  vdwmc2  16950  odcau  19534  fidomndrnglem  20681  islss  20840  obs2ss  21638  obslbs  21639  dsmmacl  21650  mvrf1  21895  mpfrcl  21992  mhpvarcl  22035  regr1lem2  23627  iccpnfhmeo  24843  itg10a  25611  dvlip  25898  deg1ge  26003  elply2  26101  coeeulem  26129  dgrle  26148  coemullem  26155  basellem2  26992  perfectlem2  27141  lgsabs1  27247  nosepon  27577  noextenddif  27580  lnon0  30727  atsseq  32276  disjif2  32510  prmidl0  33421  cvmseu  35263  matunitlindf  37612  poimirlem2  37616  poimirlem18  37632  poimirlem21  37635  itg2addnclem  37665  lsatcmp  38996  lsatcmp2  38997  ltrnnid  40130  trlatn0  40166  cdlemh  40811  dochlkr  41379  perfectALTVlem2  47723