Theorem necon4ad 2957

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  necon1d  2960  fisseneq  9291  f1finf1o  9303  f1finf1oOLD  9304  dfac5  10167  isf32lem9  10399  fpwwe2  10681  qextlt  13242  qextle  13243  xsubge0  13300  hashf1  14493  climuni  15585  rpnnen2lem12  16258  fzo0dvdseq  16357  4sqlem11  16989  haust1  23376  deg1lt0  26145  ply1divmo  26190  ig1peu  26229  dgrlt  26321  quotcan  26366  fta  27138  atcv0eq  32408  erdszelem9  35184  poimirlem23  37630  poimir  37640  lshpdisj  38969  lsatcv0eq  39029  exatleN  39387  atcvr0eq  39409  cdlemg31c  40682  itrere  42332  sn-itrere  42475  sn-retire  42476  jm2.19  42982  jm2.26lem3  42990  dgraa0p  43138