Theorem necon1ad 2973

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1568   ≠ wne 2956

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 210  df-ne 2957

This theorem is referenced by:  prnebg  4820  fr0  5639  sofld  6185  onmindif2  7805  suppss  8189  suppss2  8195  uniinqs  8794  dfac5lem4  10109  uzwo  12934  seqf1olem1  14076  seqf1olem2  14077  hashnncl  14401  pceq0  16930  vdwmc2  17038  odcau  19673  fidomndrnglem  20855  islss  21034  prmidl0  21457  obs2ss  21858  obslbs  21859  dsmmacl  21870  mvrf1  22114  mpfrcl  22215  mhpvarcl  22290  regr1lem2  23876  iccpnfhmeo  25083  itg10a  25848  dvlip  26131  deg1ge  26234  elply2  26332  coeeulem  26360  dgrle  26379  coemullem  26386  basellem2  27222  perfectlem2  27370  lgsabs1  27476  nosepon  27805  noextenddif  27808  lnon0  31116  atsseq  32665  disjif2  32892  cvmseu  35722  matunitlindf  38213  poimirlem2  38217  poimirlem18  38233  poimirlem21  38236  itg2addnclem  38266  lsatcmp  39723  lsatcmp2  39724  ltrnnid  40856  trlatn0  40892  cdlemh  41537  dochlkr  42105  perfectALTVlem2  48432