Theorem necon1ad 2976

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  prnebg  4814  fr0  5633  sofld  6191  onmindif2  7845  suppss  8239  suppss2  8245  uniinqs  8846  dfac5lem4  10232  uzwo  13065  seqf1olem1  14211  seqf1olem2  14212  hashnncl  14537  pceq0  17078  vdwmc2  17186  odcau  19848  fidomndrnglem  21060  islss  21239  prmidl0  21664  obs2ss  22065  obslbs  22066  dsmmacl  22077  mvrf1  22323  mpfrcl  22424  mhpvarcl  22499  matunitlindf  23026  regr1lem2  24089  iccpnfhmeo  25296  itg10a  26061  dvlip  26343  deg1ge  26446  elply2  26544  coeeulem  26573  dgrle  26592  coemullem  26599  basellem2  27439  perfectlem2  27587  lgsabs1  27693  nosepon  28052  noextenddif  28055  lnon0  31430  atsseq  32979  disjif2  33247  cvmseu  36208  poimirlem2  38732  poimirlem18  38748  poimirlem21  38751  itg2addnclem  38781  lsatcmp  40252  lsatcmp2  40253  ltrnnid  41385  trlatn0  41421  cdlemh  42066  dochlkr  42634  perfectALTVlem2  49025