Theorem necon4ad 2951

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 2950	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵))
4	1, 3	syl5 34	1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))

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

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 2933

This theorem is referenced by:  necon1d  2954  fisseneq  9163  f1finf1o  9173  dfac5  10039  isf32lem9  10271  fpwwe2  10554  qextlt  13118  qextle  13119  xsubge0  13176  hashf1  14380  climuni  15475  rpnnen2lem12  16150  fzo0dvdseq  16250  4sqlem11  16883  haust1  23296  deg1lt0  26052  ply1divmo  26097  ig1peu  26136  dgrlt  26228  quotcan  26273  fta  27046  atcv0eq  32454  erdszelem9  35393  poimirlem23  37840  poimir  37850  lshpdisj  39243  lsatcv0eq  39303  exatleN  39660  atcvr0eq  39682  cdlemg31c  40955  sn-itrere  42739  sn-retire  42740  jm2.19  43231  jm2.26lem3  43239  dgraa0p  43387