Theorem necon4ad 2971

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

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

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 2953

This theorem is referenced by:  necon1d  2974  fisseneq  8781  f1finf1o  8796  dfac5  9602  isf32lem9  9835  fpwwe2  10117  qextlt  12651  qextle  12652  xsubge0  12709  hashf1  13881  climuni  14971  rpnnen2lem12  15640  fzo0dvdseq  15738  4sqlem11  16361  haust1  22067  deg1lt0  24806  ply1divmo  24850  ig1peu  24886  dgrlt  24977  quotcan  25019  fta  25779  atcv0eq  30276  erdszelem9  32691  poimirlem23  35396  poimir  35406  lshpdisj  36599  lsatcv0eq  36659  exatleN  37016  atcvr0eq  37038  cdlemg31c  38311  itrere  39979  retire  39980  jm2.19  40353  jm2.26lem3  40361  dgraa0p  40512