Theorem necon1ad 2946

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  prnebg  4807  fr0  5597  sofld  6139  onmindif2  7746  suppss  8130  suppss2  8136  uniinqs  8727  dfac5lem4  10024  dfac5lem4OLD  10026  uzwo  12811  seqf1olem1  13950  seqf1olem2  13951  hashnncl  14275  pceq0  16785  vdwmc2  16893  odcau  19518  fidomndrnglem  20689  islss  20869  obs2ss  21668  obslbs  21669  dsmmacl  21680  mvrf1  21924  mpfrcl  22021  mhpvarcl  22064  regr1lem2  23656  iccpnfhmeo  24871  itg10a  25639  dvlip  25926  deg1ge  26031  elply2  26129  coeeulem  26157  dgrle  26176  coemullem  26183  basellem2  27020  perfectlem2  27169  lgsabs1  27275  nosepon  27605  noextenddif  27608  lnon0  30780  atsseq  32329  disjif2  32563  prmidl0  33422  cvmseu  35341  matunitlindf  37678  poimirlem2  37682  poimirlem18  37698  poimirlem21  37701  itg2addnclem  37731  lsatcmp  39122  lsatcmp2  39123  ltrnnid  40255  trlatn0  40291  cdlemh  40936  dochlkr  41504  perfectALTVlem2  47846