Theorem necon1ad 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  prnebg  4860  fr0  5666  sofld  6208  onmindif2  7826  suppss  8217  suppss2  8223  uniinqs  8835  dfac5lem4  10163  dfac5lem4OLD  10165  uzwo  12950  seqf1olem1  14078  seqf1olem2  14079  hashnncl  14401  pceq0  16904  vdwmc2  17012  odcau  19636  fidomndrnglem  20789  islss  20949  obs2ss  21766  obslbs  21767  dsmmacl  21778  mvrf1  22023  mpfrcl  22126  mhpvarcl  22169  regr1lem2  23763  iccpnfhmeo  24989  itg10a  25759  dvlip  26046  deg1ge  26151  elply2  26249  coeeulem  26277  dgrle  26296  coemullem  26303  basellem2  27139  perfectlem2  27288  lgsabs1  27394  nosepon  27724  noextenddif  27727  lnon0  30826  atsseq  32375  disjif2  32600  prmidl0  33457  cvmseu  35260  matunitlindf  37604  poimirlem2  37608  poimirlem18  37624  poimirlem21  37627  itg2addnclem  37657  lsatcmp  38984  lsatcmp2  38985  ltrnnid  40118  trlatn0  40154  cdlemh  40799  dochlkr  41367  perfectALTVlem2  47646