Theorem necon1ad 2973

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

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

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 2957

This theorem is used by:  prnebg  4816  fr0  5629  sofld  6178  onmindif2  7810  suppss  8195  suppss2  8201  uniinqs  8802  dfac5lem4  10186  uzwo  13019  seqf1olem1  14164  seqf1olem2  14165  hashnncl  14490  pceq0  17029  vdwmc2  17137  odcau  19798  fidomndrnglem  21010  islss  21189  prmidl0  21614  obs2ss  22015  obslbs  22016  dsmmacl  22027  mvrf1  22273  mpfrcl  22374  mhpvarcl  22449  matunitlindf  22976  regr1lem2  24039  iccpnfhmeo  25246  itg10a  26011  dvlip  26293  deg1ge  26396  elply2  26494  coeeulem  26523  dgrle  26542  coemullem  26549  basellem2  27391  perfectlem2  27539  lgsabs1  27645  nosepon  28004  noextenddif  28007  lnon0  31382  atsseq  32931  disjif2  33157  cvmseu  36010  poimirlem2  38508  poimirlem18  38524  poimirlem21  38527  itg2addnclem  38557  lsatcmp  40028  lsatcmp2  40029  ltrnnid  41161  trlatn0  41197  cdlemh  41842  dochlkr  42410  perfectALTVlem2  48764