Theorem necon1ad 2811

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  prnebg  4389  fr0  5093  sofld  5581  onmindif2  7012  suppss  7325  suppss2  7329  uniinqs  7827  dfac5lem4  8949  uzwo  11751  seqf1olem1  12840  seqf1olem2  12841  hashnncl  13157  pceq0  15575  vdwmc2  15683  odcau  18019  islss  18935  fidomndrnglem  19306  mvrf1  19425  mpfrcl  19518  obs2ss  20073  obslbs  20074  dsmmacl  20085  regr1lem2  21543  iccpnfhmeo  22744  itg10a  23477  dvlip  23756  deg1ge  23858  elply2  23952  coeeulem  23980  dgrle  23999  coemullem  24006  basellem2  24808  perfectlem2  24955  lgsabs1  25061  lnon0  27653  atsseq  29206  disjif2  29394  cvmseu  31258  nosepon  31818  noextenddif  31821  matunitlindf  33407  poimirlem2  33411  poimirlem18  33427  poimirlem21  33430  itg2addnclem  33461  lsatcmp  34290  lsatcmp2  34291  ltrnnid  35422  trlatn0  35459  cdlemh  36105  dochlkr  36674  perfectALTVlem2  41631