Theorem necon1ad 2977

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 2961

This theorem is referenced by:  prnebg  4817  fr0  5630  sofld  6177  onmindif2  7794  suppss  8178  suppss2  8184  uniinqs  8783  dfac5lem4  10098  uzwo  12926  seqf1olem1  14068  seqf1olem2  14069  hashnncl  14393  pceq0  16921  vdwmc2  17029  odcau  19665  fidomndrnglem  20845  islss  21024  prmidl0  21438  obs2ss  21839  obslbs  21840  dsmmacl  21851  mvrf1  22095  mpfrcl  22196  mhpvarcl  22271  regr1lem2  23858  iccpnfhmeo  25065  itg10a  25830  dvlip  26113  deg1ge  26216  elply2  26314  coeeulem  26342  dgrle  26361  coemullem  26368  basellem2  27204  perfectlem2  27352  lgsabs1  27458  nosepon  27787  noextenddif  27790  lnon0  31059  atsseq  32608  disjif2  32836  cvmseu  35639  matunitlindf  38129  poimirlem2  38133  poimirlem18  38149  poimirlem21  38152  itg2addnclem  38182  lsatcmp  39639  lsatcmp2  39640  ltrnnid  40772  trlatn0  40808  cdlemh  41453  dochlkr  42021  perfectALTVlem2  48342