Theorem necon1ad 2959

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 206  df-ne 2943

This theorem is referenced by:  prnebg  4783  fr0  5559  sofld  6079  onmindif2  7634  suppss  7981  suppssOLD  7982  suppss2  7987  uniinqs  8544  dfac5lem4  9813  uzwo  12580  seqf1olem1  13690  seqf1olem2  13691  hashnncl  14009  pceq0  16500  vdwmc2  16608  odcau  19124  islss  20111  fidomndrnglem  20491  obs2ss  20846  obslbs  20847  dsmmacl  20858  mvrf1  21104  mpfrcl  21205  mhpvarcl  21248  regr1lem2  22799  iccpnfhmeo  24014  itg10a  24780  dvlip  25062  deg1ge  25168  elply2  25262  coeeulem  25290  dgrle  25309  coemullem  25316  basellem2  26136  perfectlem2  26283  lgsabs1  26389  lnon0  29061  atsseq  30610  disjif2  30821  prmidl0  31528  cvmseu  33138  nosepon  33795  noextenddif  33798  matunitlindf  35702  poimirlem2  35706  poimirlem18  35722  poimirlem21  35725  itg2addnclem  35755  lsatcmp  36944  lsatcmp2  36945  ltrnnid  38077  trlatn0  38113  cdlemh  38758  dochlkr  39326  perfectALTVlem2  45062