Theorem necon1ad 2955

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

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

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 2939

This theorem is referenced by:  prnebg  4855  fr0  5654  sofld  6185  onmindif2  7797  suppss  8181  suppssOLD  8182  suppss2  8187  uniinqs  8793  dfac5lem4  10123  uzwo  12899  seqf1olem1  14011  seqf1olem2  14012  hashnncl  14330  pceq0  16808  vdwmc2  16916  odcau  19513  islss  20689  fidomndrnglem  21125  obs2ss  21503  obslbs  21504  dsmmacl  21515  mvrf1  21764  mpfrcl  21867  mhpvarcl  21910  regr1lem2  23464  iccpnfhmeo  24690  itg10a  25460  dvlip  25745  deg1ge  25851  elply2  25945  coeeulem  25973  dgrle  25992  coemullem  25999  basellem2  26822  perfectlem2  26969  lgsabs1  27075  nosepon  27404  noextenddif  27407  lnon0  30318  atsseq  31867  disjif2  32079  prmidl0  32843  cvmseu  34565  matunitlindf  36789  poimirlem2  36793  poimirlem18  36809  poimirlem21  36812  itg2addnclem  36842  lsatcmp  38176  lsatcmp2  38177  ltrnnid  39310  trlatn0  39346  cdlemh  39991  dochlkr  40559  perfectALTVlem2  46688