Theorem necon1ad 2957

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

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

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 2941

This theorem is referenced by:  prnebg  4856  fr0  5663  sofld  6207  onmindif2  7827  suppss  8219  suppss2  8225  uniinqs  8837  dfac5lem4  10166  dfac5lem4OLD  10168  uzwo  12953  seqf1olem1  14082  seqf1olem2  14083  hashnncl  14405  pceq0  16909  vdwmc2  17017  odcau  19622  fidomndrnglem  20773  islss  20932  obs2ss  21749  obslbs  21750  dsmmacl  21761  mvrf1  22006  mpfrcl  22109  mhpvarcl  22152  regr1lem2  23748  iccpnfhmeo  24976  itg10a  25745  dvlip  26032  deg1ge  26137  elply2  26235  coeeulem  26263  dgrle  26282  coemullem  26289  basellem2  27125  perfectlem2  27274  lgsabs1  27380  nosepon  27710  noextenddif  27713  lnon0  30817  atsseq  32366  disjif2  32594  prmidl0  33478  cvmseu  35281  matunitlindf  37625  poimirlem2  37629  poimirlem18  37645  poimirlem21  37648  itg2addnclem  37678  lsatcmp  39004  lsatcmp2  39005  ltrnnid  40138  trlatn0  40174  cdlemh  40819  dochlkr  41387  perfectALTVlem2  47709