Theorem necon4ad 2958

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

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

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 2940

This theorem is referenced by:  necon1d  2961  fisseneq  9294  f1finf1o  9306  f1finf1oOLD  9307  dfac5  10170  isf32lem9  10402  fpwwe2  10684  qextlt  13246  qextle  13247  xsubge0  13304  hashf1  14497  climuni  15589  rpnnen2lem12  16262  fzo0dvdseq  16361  4sqlem11  16994  haust1  23361  deg1lt0  26131  ply1divmo  26176  ig1peu  26215  dgrlt  26307  quotcan  26352  fta  27124  atcv0eq  32399  erdszelem9  35205  poimirlem23  37651  poimir  37661  lshpdisj  38989  lsatcv0eq  39049  exatleN  39407  atcvr0eq  39429  cdlemg31c  40702  itrere  42358  sn-itrere  42503  sn-retire  42504  jm2.19  43010  jm2.26lem3  43018  dgraa0p  43166