Theorem necon1ad 2958

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  prnebg  4857  fr0  5656  sofld  6187  onmindif2  7795  suppss  8179  suppssOLD  8180  suppss2  8185  uniinqs  8791  dfac5lem4  10121  uzwo  12895  seqf1olem1  14007  seqf1olem2  14008  hashnncl  14326  pceq0  16804  vdwmc2  16912  odcau  19472  islss  20545  fidomndrnglem  20925  obs2ss  21284  obslbs  21285  dsmmacl  21296  mvrf1  21545  mpfrcl  21648  mhpvarcl  21691  regr1lem2  23244  iccpnfhmeo  24461  itg10a  25228  dvlip  25510  deg1ge  25616  elply2  25710  coeeulem  25738  dgrle  25757  coemullem  25764  basellem2  26586  perfectlem2  26733  lgsabs1  26839  nosepon  27168  noextenddif  27171  lnon0  30051  atsseq  31600  disjif2  31812  prmidl0  32569  cvmseu  34267  matunitlindf  36486  poimirlem2  36490  poimirlem18  36506  poimirlem21  36509  itg2addnclem  36539  lsatcmp  37873  lsatcmp2  37874  ltrnnid  39007  trlatn0  39043  cdlemh  39688  dochlkr  40256  perfectALTVlem2  46390