Theorem necon1ad 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1632   ≠ wne 2932

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 197  df-ne 2933

This theorem is referenced by:  prnebg  4533  fr0  5245  sofld  5739  onmindif2  7178  suppss  7495  suppss2  7499  uniinqs  7996  dfac5lem4  9159  uzwo  11964  seqf1olem1  13054  seqf1olem2  13055  hashnncl  13369  pceq0  15797  vdwmc2  15905  odcau  18239  islss  19157  fidomndrnglem  19528  mvrf1  19647  mpfrcl  19740  obs2ss  20295  obslbs  20296  dsmmacl  20307  regr1lem2  21765  iccpnfhmeo  22965  itg10a  23696  dvlip  23975  deg1ge  24077  elply2  24171  coeeulem  24199  dgrle  24218  coemullem  24225  basellem2  25028  perfectlem2  25175  lgsabs1  25281  lnon0  27983  atsseq  29536  disjif2  29722  cvmseu  31586  nosepon  32145  noextenddif  32148  matunitlindf  33738  poimirlem2  33742  poimirlem18  33758  poimirlem21  33761  itg2addnclem  33792  lsatcmp  34811  lsatcmp2  34812  ltrnnid  35943  trlatn0  35980  cdlemh  36625  dochlkr  37194  perfectALTVlem2  42159