Theorem necon1ad 3004

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 2988

This theorem is referenced by:  prnebg  4746  fr0  5498  sofld  6011  onmindif2  7507  suppss  7843  suppss2  7847  uniinqs  8360  dfac5lem4  9537  uzwo  12299  seqf1olem1  13405  seqf1olem2  13406  hashnncl  13723  pceq0  16197  vdwmc2  16305  odcau  18721  islss  19699  fidomndrnglem  20072  obs2ss  20418  obslbs  20419  dsmmacl  20430  mvrf1  20663  mpfrcl  20757  mhpvarcl  20798  regr1lem2  22345  iccpnfhmeo  23550  itg10a  24314  dvlip  24596  deg1ge  24699  elply2  24793  coeeulem  24821  dgrle  24840  coemullem  24847  basellem2  25667  perfectlem2  25814  lgsabs1  25920  lnon0  28581  atsseq  30130  disjif2  30344  prmidl0  31034  cvmseu  32636  nosepon  33285  noextenddif  33288  matunitlindf  35055  poimirlem2  35059  poimirlem18  35075  poimirlem21  35078  itg2addnclem  35108  lsatcmp  36299  lsatcmp2  36300  ltrnnid  37432  trlatn0  37468  cdlemh  38113  dochlkr  38681  perfectALTVlem2  44240