Theorem necon1ad 2978

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

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

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 2962

This theorem is used by:  prnebg  4826  fr0  5644  sofld  6190  onmindif2  7815  suppss  8199  suppss2  8205  uniinqs  8804  dfac5lem4  10129  uzwo  12953  seqf1olem1  14097  seqf1olem2  14098  hashnncl  14422  pceq0  16956  vdwmc2  17064  odcau  19705  fidomndrnglem  20913  islss  21092  prmidl0  21515  obs2ss  21916  obslbs  21917  dsmmacl  21928  mvrf1  22172  mpfrcl  22273  mhpvarcl  22348  regr1lem2  23934  iccpnfhmeo  25141  itg10a  25906  dvlip  26189  deg1ge  26292  elply2  26390  coeeulem  26418  dgrle  26437  coemullem  26444  basellem2  27283  perfectlem2  27431  lgsabs1  27537  nosepon  27866  noextenddif  27869  lnon0  31187  atsseq  32736  disjif2  32963  cvmseu  35789  matunitlindf  38310  poimirlem2  38314  poimirlem18  38330  poimirlem21  38333  itg2addnclem  38363  lsatcmp  39818  lsatcmp2  39819  ltrnnid  40951  trlatn0  40987  cdlemh  41632  dochlkr  42200  perfectALTVlem2  48528