Theorem necon1ad 2961

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

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

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 2945

This theorem is referenced by:  prnebg  4787  fr0  5569  sofld  6095  onmindif2  7666  suppss  8019  suppssOLD  8020  suppss2  8025  uniinqs  8595  dfac5lem4  9891  uzwo  12660  seqf1olem1  13771  seqf1olem2  13772  hashnncl  14090  pceq0  16581  vdwmc2  16689  odcau  19218  islss  20205  fidomndrnglem  20587  obs2ss  20945  obslbs  20946  dsmmacl  20957  mvrf1  21203  mpfrcl  21304  mhpvarcl  21347  regr1lem2  22900  iccpnfhmeo  24117  itg10a  24884  dvlip  25166  deg1ge  25272  elply2  25366  coeeulem  25394  dgrle  25413  coemullem  25420  basellem2  26240  perfectlem2  26387  lgsabs1  26493  lnon0  29169  atsseq  30718  disjif2  30929  prmidl0  31635  cvmseu  33247  nosepon  33877  noextenddif  33880  matunitlindf  35784  poimirlem2  35788  poimirlem18  35804  poimirlem21  35807  itg2addnclem  35837  lsatcmp  37024  lsatcmp2  37025  ltrnnid  38157  trlatn0  38193  cdlemh  38838  dochlkr  39406  perfectALTVlem2  45185