Theorem necon4ad 2944

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon1d  2947  fisseneq  9162  f1finf1o  9174  f1finf1oOLD  9175  dfac5  10042  isf32lem9  10274  fpwwe2  10556  qextlt  13123  qextle  13124  xsubge0  13181  hashf1  14382  climuni  15477  rpnnen2lem12  16152  fzo0dvdseq  16252  4sqlem11  16885  haust1  23255  deg1lt0  26012  ply1divmo  26057  ig1peu  26096  dgrlt  26188  quotcan  26233  fta  27006  atcv0eq  32341  erdszelem9  35171  poimirlem23  37622  poimir  37632  lshpdisj  38965  lsatcv0eq  39025  exatleN  39383  atcvr0eq  39405  cdlemg31c  40678  sn-itrere  42461  sn-retire  42462  jm2.19  42966  jm2.26lem3  42974  dgraa0p  43122