Theorem necon1ad 2972

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  prnebg  4810  fr0  5628  sofld  6178  onmindif2  7821  suppss  8214  suppss2  8220  uniinqs  8821  dfac5lem4  10208  uzwo  13041  seqf1olem1  14187  seqf1olem2  14188  hashnncl  14513  pceq0  17054  vdwmc2  17162  odcau  19823  fidomndrnglem  21035  islss  21214  prmidl0  21639  obs2ss  22040  obslbs  22041  dsmmacl  22052  mvrf1  22298  mpfrcl  22399  mhpvarcl  22474  matunitlindf  23001  regr1lem2  24064  iccpnfhmeo  25271  itg10a  26036  dvlip  26318  deg1ge  26421  elply2  26519  coeeulem  26548  dgrle  26567  coemullem  26574  basellem2  27414  perfectlem2  27562  lgsabs1  27668  nosepon  28027  noextenddif  28030  lnon0  31405  atsseq  32954  disjif2  33222  cvmseu  36127  poimirlem2  38633  poimirlem18  38649  poimirlem21  38652  itg2addnclem  38682  lsatcmp  40153  lsatcmp2  40154  ltrnnid  41286  trlatn0  41322  cdlemh  41967  dochlkr  42535  perfectALTVlem2  48913