Theorem necon1ad 2988

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1653   ≠ wne 2971

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 199  df-ne 2972

This theorem is referenced by:  prnebg  4574  fr0  5291  sofld  5798  onmindif2  7246  suppss  7563  suppss2  7567  uniinqs  8065  dfac5lem4  9235  uzwo  11996  seqf1olem1  13094  seqf1olem2  13095  hashnncl  13407  pceq0  15908  vdwmc2  16016  odcau  18332  islss  19253  fidomndrnglem  19629  mvrf1  19748  mpfrcl  19840  obs2ss  20398  obslbs  20399  dsmmacl  20410  regr1lem2  21872  iccpnfhmeo  23072  itg10a  23818  dvlip  24097  deg1ge  24199  elply2  24293  coeeulem  24321  dgrle  24340  coemullem  24347  basellem2  25160  perfectlem2  25307  lgsabs1  25413  lnon0  28178  atsseq  29731  disjif2  29911  cvmseu  31775  nosepon  32331  noextenddif  32334  matunitlindf  33896  poimirlem2  33900  poimirlem18  33916  poimirlem21  33919  itg2addnclem  33949  lsatcmp  35024  lsatcmp2  35025  ltrnnid  36157  trlatn0  36193  cdlemh  36838  dochlkr  37406  perfectALTVlem2  42413