Theorem necon1ad 2950

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

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

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 2934

This theorem is referenced by:  prnebg  4800  fr0  5602  sofld  6145  onmindif2  7754  suppss  8137  suppss2  8143  uniinqs  8737  dfac5lem4  10039  dfac5lem4OLD  10041  uzwo  12852  seqf1olem1  13994  seqf1olem2  13995  hashnncl  14319  pceq0  16833  vdwmc2  16941  odcau  19570  fidomndrnglem  20740  islss  20920  obs2ss  21719  obslbs  21720  dsmmacl  21731  mvrf1  21974  mpfrcl  22073  mhpvarcl  22124  regr1lem2  23715  iccpnfhmeo  24922  itg10a  25687  dvlip  25970  deg1ge  26073  elply2  26171  coeeulem  26199  dgrle  26218  coemullem  26225  basellem2  27059  perfectlem2  27207  lgsabs1  27313  nosepon  27643  noextenddif  27646  lnon0  30884  atsseq  32433  disjif2  32666  prmidl0  33525  cvmseu  35474  matunitlindf  37953  poimirlem2  37957  poimirlem18  37973  poimirlem21  37976  itg2addnclem  38006  lsatcmp  39463  lsatcmp2  39464  ltrnnid  40596  trlatn0  40632  cdlemh  41277  dochlkr  41845  perfectALTVlem2  48210