Theorem necon1ad 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  prnebg  4799  fr0  5609  sofld  6151  onmindif2  7761  suppss  8144  suppss2  8150  uniinqs  8744  dfac5lem4  10048  dfac5lem4OLD  10050  uzwo  12861  seqf1olem1  14003  seqf1olem2  14004  hashnncl  14328  pceq0  16842  vdwmc2  16950  odcau  19579  fidomndrnglem  20749  islss  20929  obs2ss  21709  obslbs  21710  dsmmacl  21721  mvrf1  21964  mpfrcl  22063  mhpvarcl  22114  regr1lem2  23705  iccpnfhmeo  24912  itg10a  25677  dvlip  25960  deg1ge  26063  elply2  26161  coeeulem  26189  dgrle  26208  coemullem  26215  basellem2  27045  perfectlem2  27193  lgsabs1  27299  nosepon  27629  noextenddif  27632  lnon0  30869  atsseq  32418  disjif2  32651  prmidl0  33510  cvmseu  35458  matunitlindf  37939  poimirlem2  37943  poimirlem18  37959  poimirlem21  37962  itg2addnclem  37992  lsatcmp  39449  lsatcmp2  39450  ltrnnid  40582  trlatn0  40618  cdlemh  41263  dochlkr  41831  perfectALTVlem2  48198