Theorem necon1ad 2974

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

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

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 2958

This theorem is used by:  prnebg  4819  fr0  5637  sofld  6184  onmindif2  7810  suppss  8196  suppss2  8202  uniinqs  8801  dfac5lem4  10133  uzwo  12964  seqf1olem1  14109  seqf1olem2  14110  hashnncl  14434  pceq0  16969  vdwmc2  17077  odcau  19737  fidomndrnglem  20945  islss  21124  prmidl0  21547  obs2ss  21948  obslbs  21949  dsmmacl  21960  mvrf1  22206  mpfrcl  22307  mhpvarcl  22382  matunitlindf  22909  regr1lem2  23972  iccpnfhmeo  25179  itg10a  25944  dvlip  26227  deg1ge  26330  elply2  26428  coeeulem  26457  dgrle  26476  coemullem  26483  basellem2  27326  perfectlem2  27474  lgsabs1  27580  nosepon  27909  noextenddif  27912  lnon0  31287  atsseq  32836  disjif2  33062  cvmseu  35863  poimirlem2  38379  poimirlem18  38395  poimirlem21  38398  itg2addnclem  38428  lsatcmp  39884  lsatcmp2  39885  ltrnnid  41017  trlatn0  41053  cdlemh  41698  dochlkr  42266  perfectALTVlem2  48646