Theorem necon1ad 2943

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

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

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 2927

This theorem is referenced by:  prnebg  4823  fr0  5619  sofld  6163  onmindif2  7786  suppss  8176  suppss2  8182  uniinqs  8773  dfac5lem4  10086  dfac5lem4OLD  10088  uzwo  12877  seqf1olem1  14013  seqf1olem2  14014  hashnncl  14338  pceq0  16849  vdwmc2  16957  odcau  19541  fidomndrnglem  20688  islss  20847  obs2ss  21645  obslbs  21646  dsmmacl  21657  mvrf1  21902  mpfrcl  21999  mhpvarcl  22042  regr1lem2  23634  iccpnfhmeo  24850  itg10a  25618  dvlip  25905  deg1ge  26010  elply2  26108  coeeulem  26136  dgrle  26155  coemullem  26162  basellem2  26999  perfectlem2  27148  lgsabs1  27254  nosepon  27584  noextenddif  27587  lnon0  30734  atsseq  32283  disjif2  32517  prmidl0  33428  cvmseu  35270  matunitlindf  37619  poimirlem2  37623  poimirlem18  37639  poimirlem21  37642  itg2addnclem  37672  lsatcmp  39003  lsatcmp2  39004  ltrnnid  40137  trlatn0  40173  cdlemh  40818  dochlkr  41386  perfectALTVlem2  47727