Theorem necon4ad 2959

Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypothesis

Ref	Expression
necon4ad.1	⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))

Assertion

Ref	Expression
necon4ad	⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))

Proof of Theorem necon4ad

Step	Hyp	Ref	Expression
1		notnot 142	. 2 ⊢ (𝜓 → ¬ ¬ 𝜓)
2		necon4ad.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))
3	2	necon1bd 2958	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵))
4	1, 3	syl5 34	1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ 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 207  df-ne 2941

This theorem is referenced by:  necon1d  2962  fisseneq  9293  f1finf1o  9305  f1finf1oOLD  9306  dfac5  10169  isf32lem9  10401  fpwwe2  10683  qextlt  13245  qextle  13246  xsubge0  13303  hashf1  14496  climuni  15588  rpnnen2lem12  16261  fzo0dvdseq  16360  4sqlem11  16993  haust1  23360  deg1lt0  26130  ply1divmo  26175  ig1peu  26214  dgrlt  26306  quotcan  26351  fta  27123  atcv0eq  32398  erdszelem9  35204  poimirlem23  37650  poimir  37660  lshpdisj  38988  lsatcv0eq  39048  exatleN  39406  atcvr0eq  39428  cdlemg31c  40701  itrere  42353  sn-itrere  42498  sn-retire  42499  jm2.19  43005  jm2.26lem3  43013  dgraa0p  43161