Theorem necon4ad 2961

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  necon1d  2964  fisseneq  8963  f1finf1o  8975  dfac5  9815  isf32lem9  10048  fpwwe2  10330  qextlt  12866  qextle  12867  xsubge0  12924  hashf1  14099  climuni  15189  rpnnen2lem12  15862  fzo0dvdseq  15960  4sqlem11  16584  haust1  22411  deg1lt0  25161  ply1divmo  25205  ig1peu  25241  dgrlt  25332  quotcan  25374  fta  26134  atcv0eq  30642  erdszelem9  33061  poimirlem23  35727  poimir  35737  lshpdisj  36928  lsatcv0eq  36988  exatleN  37345  atcvr0eq  37367  cdlemg31c  38640  itrere  40357  retire  40358  jm2.19  40731  jm2.26lem3  40739  dgraa0p  40890