Theorem necon1ad 2951

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

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

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 210  df-ne 2935

This theorem is referenced by:  prnebg  4741  fr0  5504  sofld  6019  onmindif2  7546  suppss  7889  suppssOLD  7890  suppss2  7895  uniinqs  8408  dfac5lem4  9626  uzwo  12393  seqf1olem1  13501  seqf1olem2  13502  hashnncl  13819  pceq0  16307  vdwmc2  16415  odcau  18847  islss  19825  fidomndrnglem  20198  obs2ss  20545  obslbs  20546  dsmmacl  20557  mvrf1  20804  mpfrcl  20899  mhpvarcl  20942  regr1lem2  22491  iccpnfhmeo  23697  itg10a  24463  dvlip  24745  deg1ge  24851  elply2  24945  coeeulem  24973  dgrle  24992  coemullem  24999  basellem2  25819  perfectlem2  25966  lgsabs1  26072  lnon0  28733  atsseq  30282  disjif2  30494  prmidl0  31198  cvmseu  32809  nosepon  33509  noextenddif  33512  matunitlindf  35398  poimirlem2  35402  poimirlem18  35418  poimirlem21  35421  itg2addnclem  35451  lsatcmp  36640  lsatcmp2  36641  ltrnnid  37773  trlatn0  37809  cdlemh  38454  dochlkr  39022  perfectALTVlem2  44708