Theorem necon1ad 2799

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  prnebg  4329  fr0  5017  sofld  5500  onmindif2  6904  suppss  7212  suppss2  7216  uniinqs  7714  dfac5lem4  8832  uzwo  11627  seqf1olem1  12702  seqf1olem2  12703  hashnncl  13018  pceq0  15413  vdwmc2  15521  odcau  17842  islss  18756  fidomndrnglem  19127  mvrf1  19246  mpfrcl  19339  obs2ss  19892  obslbs  19893  dsmmacl  19904  regr1lem2  21353  iccpnfhmeo  22552  itg10a  23283  dvlip  23560  deg1ge  23662  elply2  23756  coeeulem  23784  dgrle  23803  coemullem  23810  basellem2  24608  perfectlem2  24755  lgsabs1  24861  lnon0  27037  atsseq  28590  disjif2  28776  cvmseu  30512  nosepon  31066  matunitlindf  32577  poimirlem2  32581  poimirlem18  32597  poimirlem21  32600  itg2addnclem  32631  lsatcmp  33308  lsatcmp2  33309  ltrnnid  34440  trlatn0  34477  cdlemh  35123  dochlkr  35692  perfectALTVlem2  40165