Theorem necon1ad 3033

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  prnebg  4785  fr0  5533  sofld  6043  onmindif2  7526  suppss  7859  suppss2  7863  uniinqs  8376  dfac5lem4  9551  uzwo  12310  seqf1olem1  13408  seqf1olem2  13409  hashnncl  13726  pceq0  16206  vdwmc2  16314  odcau  18728  islss  19705  fidomndrnglem  20078  mvrf1  20204  mpfrcl  20297  obs2ss  20872  obslbs  20873  dsmmacl  20884  regr1lem2  22347  iccpnfhmeo  23548  itg10a  24310  dvlip  24589  deg1ge  24691  elply2  24785  coeeulem  24813  dgrle  24832  coemullem  24839  basellem2  25658  perfectlem2  25805  lgsabs1  25911  lnon0  28574  atsseq  30123  disjif2  30330  cvmseu  32523  nosepon  33172  noextenddif  33175  matunitlindf  34889  poimirlem2  34893  poimirlem18  34909  poimirlem21  34912  itg2addnclem  34942  lsatcmp  36138  lsatcmp2  36139  ltrnnid  37271  trlatn0  37307  cdlemh  37952  dochlkr  38520  perfectALTVlem2  43886