Theorem necon1ad 2963

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  prnebg  4880  fr0  5678  sofld  6218  onmindif2  7843  suppss  8235  suppss2  8241  uniinqs  8855  dfac5lem4  10195  dfac5lem4OLD  10197  uzwo  12976  seqf1olem1  14092  seqf1olem2  14093  hashnncl  14415  pceq0  16918  vdwmc2  17026  odcau  19646  fidomndrnglem  20795  islss  20955  obs2ss  21772  obslbs  21773  dsmmacl  21784  mvrf1  22029  mpfrcl  22132  mhpvarcl  22175  regr1lem2  23769  iccpnfhmeo  24995  itg10a  25765  dvlip  26052  deg1ge  26157  elply2  26255  coeeulem  26283  dgrle  26302  coemullem  26309  basellem2  27143  perfectlem2  27292  lgsabs1  27398  nosepon  27728  noextenddif  27731  lnon0  30830  atsseq  32379  disjif2  32603  prmidl0  33443  cvmseu  35244  matunitlindf  37578  poimirlem2  37582  poimirlem18  37598  poimirlem21  37601  itg2addnclem  37631  lsatcmp  38959  lsatcmp2  38960  ltrnnid  40093  trlatn0  40129  cdlemh  40774  dochlkr  41342  perfectALTVlem2  47596