Theorem necon1ad 2942

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

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

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 2926

This theorem is referenced by:  prnebg  4807  fr0  5597  sofld  6136  onmindif2  7743  suppss  8127  suppss2  8133  uniinqs  8724  dfac5lem4  10020  dfac5lem4OLD  10022  uzwo  12812  seqf1olem1  13948  seqf1olem2  13949  hashnncl  14273  pceq0  16783  vdwmc2  16891  odcau  19483  fidomndrnglem  20657  islss  20837  obs2ss  21636  obslbs  21637  dsmmacl  21648  mvrf1  21893  mpfrcl  21990  mhpvarcl  22033  regr1lem2  23625  iccpnfhmeo  24841  itg10a  25609  dvlip  25896  deg1ge  26001  elply2  26099  coeeulem  26127  dgrle  26146  coemullem  26153  basellem2  26990  perfectlem2  27139  lgsabs1  27245  nosepon  27575  noextenddif  27578  lnon0  30742  atsseq  32291  disjif2  32525  prmidl0  33388  cvmseu  35259  matunitlindf  37608  poimirlem2  37612  poimirlem18  37628  poimirlem21  37631  itg2addnclem  37661  lsatcmp  38992  lsatcmp2  38993  ltrnnid  40125  trlatn0  40161  cdlemh  40806  dochlkr  41374  perfectALTVlem2  47716