Theorem necon1ad 2945

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  prnebg  4808  fr0  5594  sofld  6134  onmindif2  7740  suppss  8124  suppss2  8130  uniinqs  8721  dfac5lem4  10014  dfac5lem4OLD  10016  uzwo  12806  seqf1olem1  13945  seqf1olem2  13946  hashnncl  14270  pceq0  16780  vdwmc2  16888  odcau  19514  fidomndrnglem  20685  islss  20865  obs2ss  21664  obslbs  21665  dsmmacl  21676  mvrf1  21921  mpfrcl  22018  mhpvarcl  22061  regr1lem2  23653  iccpnfhmeo  24868  itg10a  25636  dvlip  25923  deg1ge  26028  elply2  26126  coeeulem  26154  dgrle  26173  coemullem  26180  basellem2  27017  perfectlem2  27166  lgsabs1  27272  nosepon  27602  noextenddif  27605  lnon0  30773  atsseq  32322  disjif2  32556  prmidl0  33410  cvmseu  35308  matunitlindf  37657  poimirlem2  37661  poimirlem18  37677  poimirlem21  37680  itg2addnclem  37710  lsatcmp  39041  lsatcmp2  39042  ltrnnid  40174  trlatn0  40210  cdlemh  40855  dochlkr  41423  perfectALTVlem2  47752