Theorem necon1ad 2953

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ≠ wne 2936

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 2937

This theorem is referenced by:  prnebg  4853  fr0  5652  sofld  6186  onmindif2  7805  suppss  8193  suppssOLD  8194  suppss2  8200  uniinqs  8810  dfac5lem4  10144  uzwo  12920  seqf1olem1  14033  seqf1olem2  14034  hashnncl  14352  pceq0  16834  vdwmc2  16942  odcau  19553  islss  20812  fidomndrnglem  21254  obs2ss  21657  obslbs  21658  dsmmacl  21669  mvrf1  21922  mpfrcl  22025  mhpvarcl  22066  regr1lem2  23638  iccpnfhmeo  24864  itg10a  25634  dvlip  25920  deg1ge  26028  elply2  26124  coeeulem  26152  dgrle  26171  coemullem  26178  basellem2  27008  perfectlem2  27157  lgsabs1  27263  nosepon  27592  noextenddif  27595  lnon0  30602  atsseq  32151  disjif2  32365  prmidl0  33161  cvmseu  34881  matunitlindf  37086  poimirlem2  37090  poimirlem18  37106  poimirlem21  37109  itg2addnclem  37139  lsatcmp  38470  lsatcmp2  38471  ltrnnid  39604  trlatn0  39640  cdlemh  40285  dochlkr  40853  perfectALTVlem2  47053