Theorem necon4ad 2977

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 143	. 2 ⊢ (𝜓 → ¬ ¬ 𝜓)
2		necon4ad.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))
3	2	necon1bd 2976	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵))
4	1, 3	syl5 35	1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  necon1d  2980  fisseneq  9224  f1finf1o  9234  dfac5  10113  isf32lem9  10346  fpwwe2  10629  qextlt  13230  qextle  13231  xsubge0  13288  hashf1  14496  climuni  15605  rpnnen2lem12  16282  fzo0dvdseq  16382  4sqlem11  17016  haust1  23490  deg1lt0  26229  ply1divmo  26274  ig1peu  26313  dgrlt  26404  quotcan  26451  fta  27222  atcv0eq  32709  erdszelem9  35669  poimirlem23  38272  poimir  38282  lshpdisj  39739  lsatcv0eq  39799  exatleN  40156  atcvr0eq  40178  cdlemg31c  41451  sn-itrere  43240  sn-retire  43241  jm2.19  43700  jm2.26lem3  43708  dgraa0p  43856