Theorem necon1ad 2975

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  prnebg  4822  fr0  5641  sofld  6187  onmindif2  7807  suppss  8191  suppss2  8197  uniinqs  8796  dfac5lem4  10111  uzwo  12936  seqf1olem1  14079  seqf1olem2  14080  hashnncl  14404  pceq0  16932  vdwmc2  17040  odcau  19675  fidomndrnglem  20857  islss  21036  prmidl0  21459  obs2ss  21860  obslbs  21861  dsmmacl  21872  mvrf1  22116  mpfrcl  22217  mhpvarcl  22292  regr1lem2  23878  iccpnfhmeo  25085  itg10a  25850  dvlip  26133  deg1ge  26236  elply2  26334  coeeulem  26362  dgrle  26381  coemullem  26388  basellem2  27224  perfectlem2  27372  lgsabs1  27478  nosepon  27807  noextenddif  27810  lnon0  31128  atsseq  32677  disjif2  32904  cvmseu  35746  matunitlindf  38247  poimirlem2  38251  poimirlem18  38267  poimirlem21  38270  itg2addnclem  38300  lsatcmp  39755  lsatcmp2  39756  ltrnnid  40888  trlatn0  40924  cdlemh  41569  dochlkr  42137  perfectALTVlem2  48464