Theorem necon1ad 2942

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  prnebg  4810  fr0  5601  sofld  6140  onmindif2  7747  suppss  8134  suppss2  8140  uniinqs  8731  dfac5lem4  10039  dfac5lem4OLD  10041  uzwo  12830  seqf1olem1  13966  seqf1olem2  13967  hashnncl  14291  pceq0  16801  vdwmc2  16909  odcau  19501  fidomndrnglem  20675  islss  20855  obs2ss  21654  obslbs  21655  dsmmacl  21666  mvrf1  21911  mpfrcl  22008  mhpvarcl  22051  regr1lem2  23643  iccpnfhmeo  24859  itg10a  25627  dvlip  25914  deg1ge  26019  elply2  26117  coeeulem  26145  dgrle  26164  coemullem  26171  basellem2  27008  perfectlem2  27157  lgsabs1  27263  nosepon  27593  noextenddif  27596  lnon0  30760  atsseq  32309  disjif2  32543  prmidl0  33397  cvmseu  35248  matunitlindf  37597  poimirlem2  37601  poimirlem18  37617  poimirlem21  37620  itg2addnclem  37650  lsatcmp  38981  lsatcmp2  38982  ltrnnid  40115  trlatn0  40151  cdlemh  40796  dochlkr  41364  perfectALTVlem2  47707