Theorem necon1ad 2957

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

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

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 206  df-ne 2941

This theorem is referenced by:  prnebg  4856  fr0  5655  sofld  6186  onmindif2  7794  suppss  8178  suppssOLD  8179  suppss2  8184  uniinqs  8790  dfac5lem4  10120  uzwo  12894  seqf1olem1  14006  seqf1olem2  14007  hashnncl  14325  pceq0  16803  vdwmc2  16911  odcau  19471  islss  20544  fidomndrnglem  20924  obs2ss  21283  obslbs  21284  dsmmacl  21295  mvrf1  21544  mpfrcl  21647  mhpvarcl  21690  regr1lem2  23243  iccpnfhmeo  24460  itg10a  25227  dvlip  25509  deg1ge  25615  elply2  25709  coeeulem  25737  dgrle  25756  coemullem  25763  basellem2  26583  perfectlem2  26730  lgsabs1  26836  nosepon  27165  noextenddif  27168  lnon0  30046  atsseq  31595  disjif2  31807  prmidl0  32564  cvmseu  34262  matunitlindf  36481  poimirlem2  36485  poimirlem18  36501  poimirlem21  36504  itg2addnclem  36534  lsatcmp  37868  lsatcmp2  37869  ltrnnid  39002  trlatn0  39038  cdlemh  39683  dochlkr  40251  perfectALTVlem2  46380