Theorem necon4ad 2979

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 2961

This theorem is referenced by:  necon1d  2982  fisseneq  9211  f1finf1o  9221  dfac5  10100  isf32lem9  10333  fpwwe2  10616  qextlt  13220  qextle  13221  xsubge0  13278  hashf1  14484  climuni  15593  rpnnen2lem12  16271  fzo0dvdseq  16371  4sqlem11  17005  haust1  23470  deg1lt0  26209  ply1divmo  26254  ig1peu  26293  dgrlt  26384  quotcan  26431  fta  27202  atcv0eq  32640  erdszelem9  35562  poimirlem23  38154  poimir  38164  lshpdisj  39623  lsatcv0eq  39683  exatleN  40040  atcvr0eq  40062  cdlemg31c  41335  sn-itrere  43122  sn-retire  43123  jm2.19  43582  jm2.26lem3  43590  dgraa0p  43738