Theorem necon1ad 2949

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

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

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 2933

This theorem is referenced by:  prnebg  4832  fr0  5632  sofld  6176  onmindif2  7799  suppss  8191  suppss2  8197  uniinqs  8809  dfac5lem4  10138  dfac5lem4OLD  10140  uzwo  12925  seqf1olem1  14057  seqf1olem2  14058  hashnncl  14382  pceq0  16889  vdwmc2  16997  odcau  19583  fidomndrnglem  20730  islss  20889  obs2ss  21687  obslbs  21688  dsmmacl  21699  mvrf1  21944  mpfrcl  22041  mhpvarcl  22084  regr1lem2  23676  iccpnfhmeo  24892  itg10a  25661  dvlip  25948  deg1ge  26053  elply2  26151  coeeulem  26179  dgrle  26198  coemullem  26205  basellem2  27042  perfectlem2  27191  lgsabs1  27297  nosepon  27627  noextenddif  27630  lnon0  30725  atsseq  32274  disjif2  32508  prmidl0  33411  cvmseu  35244  matunitlindf  37588  poimirlem2  37592  poimirlem18  37608  poimirlem21  37611  itg2addnclem  37641  lsatcmp  38967  lsatcmp2  38968  ltrnnid  40101  trlatn0  40137  cdlemh  40782  dochlkr  41350  perfectALTVlem2  47684