Theorem necon1ad 2952

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  prnebg  4794  fr0  5603  sofld  6145  onmindif2  7757  suppss  8141  suppss2  8147  uniinqs  8741  dfac5lem4  10046  dfac5lem4OLD  10048  uzwo  12859  seqf1olem1  14001  seqf1olem2  14002  hashnncl  14326  pceq0  16840  vdwmc2  16948  odcau  19577  fidomndrnglem  20751  islss  20931  obs2ss  21711  obslbs  21712  dsmmacl  21723  mvrf1  21967  mpfrcl  22068  mhpvarcl  22143  regr1lem2  23730  iccpnfhmeo  24937  itg10a  25702  dvlip  25985  deg1ge  26088  elply2  26186  coeeulem  26214  dgrle  26233  coemullem  26240  basellem2  27070  perfectlem2  27218  lgsabs1  27324  nosepon  27654  noextenddif  27657  lnon0  30894  atsseq  32443  disjif2  32677  prmidl0  33540  cvmseu  35511  matunitlindf  37992  poimirlem2  37996  poimirlem18  38012  poimirlem21  38015  itg2addnclem  38045  lsatcmp  39502  lsatcmp2  39503  ltrnnid  40635  trlatn0  40671  cdlemh  41316  dochlkr  41884  perfectALTVlem2  48220