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  4814  fr0  5610  sofld  6153  onmindif2  7762  suppss  8146  suppss2  8152  uniinqs  8746  dfac5lem4  10048  dfac5lem4OLD  10050  uzwo  12836  seqf1olem1  13976  seqf1olem2  13977  hashnncl  14301  pceq0  16811  vdwmc2  16919  odcau  19545  fidomndrnglem  20717  islss  20897  obs2ss  21696  obslbs  21697  dsmmacl  21708  mvrf1  21953  mpfrcl  22052  mhpvarcl  22103  regr1lem2  23696  iccpnfhmeo  24911  itg10a  25679  dvlip  25966  deg1ge  26071  elply2  26169  coeeulem  26197  dgrle  26216  coemullem  26223  basellem2  27060  perfectlem2  27209  lgsabs1  27315  nosepon  27645  noextenddif  27648  lnon0  30885  atsseq  32434  disjif2  32667  prmidl0  33542  cvmseu  35489  matunitlindf  37863  poimirlem2  37867  poimirlem18  37883  poimirlem21  37886  itg2addnclem  37916  lsatcmp  39373  lsatcmp2  39374  ltrnnid  40506  trlatn0  40542  cdlemh  41187  dochlkr  41755  perfectALTVlem2  48076