Theorem necon1ad 2793

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1474   ≠ wne 2774

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 195  df-ne 2776

This theorem is referenced by:  prnebg  4319  fr0  5002  sofld  5481  onmindif2  6876  suppss  7184  suppss2  7188  uniinqs  7686  dfac5lem4  8804  uzwo  11578  seqf1olem1  12652  seqf1olem2  12653  hashnncl  12965  pceq0  15354  vdwmc2  15462  odcau  17783  islss  18697  fidomndrnglem  19068  mvrf1  19187  mpfrcl  19280  obs2ss  19829  obslbs  19830  dsmmacl  19841  regr1lem2  21290  iccpnfhmeo  22478  itg10a  23195  dvlip  23472  deg1ge  23574  elply2  23668  coeeulem  23696  dgrle  23715  coemullem  23722  basellem2  24520  perfectlem2  24667  lgsabs1  24773  lnon0  26838  atsseq  28391  disjif2  28577  cvmseu  30313  nosepon  30867  matunitlindf  32375  poimirlem2  32379  poimirlem18  32395  poimirlem21  32398  itg2addnclem  32429  lsatcmp  33106  lsatcmp2  33107  ltrnnid  34238  trlatn0  34275  cdlemh  34921  dochlkr  35490  perfectALTVlem2  39965