Theorem necon1ad 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  prnebg  4812  fr0  5602  sofld  6145  onmindif2  7752  suppss  8136  suppss2  8142  uniinqs  8734  dfac5lem4  10036  dfac5lem4OLD  10038  uzwo  12824  seqf1olem1  13964  seqf1olem2  13965  hashnncl  14289  pceq0  16799  vdwmc2  16907  odcau  19533  fidomndrnglem  20705  islss  20885  obs2ss  21684  obslbs  21685  dsmmacl  21696  mvrf1  21941  mpfrcl  22040  mhpvarcl  22091  regr1lem2  23684  iccpnfhmeo  24899  itg10a  25667  dvlip  25954  deg1ge  26059  elply2  26157  coeeulem  26185  dgrle  26204  coemullem  26211  basellem2  27048  perfectlem2  27197  lgsabs1  27303  nosepon  27633  noextenddif  27636  lnon0  30873  atsseq  32422  disjif2  32656  prmidl0  33531  cvmseu  35470  matunitlindf  37815  poimirlem2  37819  poimirlem18  37835  poimirlem21  37838  itg2addnclem  37868  lsatcmp  39259  lsatcmp2  39260  ltrnnid  40392  trlatn0  40428  cdlemh  41073  dochlkr  41641  perfectALTVlem2  47964