Theorem necon4ad 3006

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 2988

This theorem is referenced by:  necon1d  3009  fisseneq  8713  f1finf1o  8729  dfac5  9539  isf32lem9  9772  fpwwe2  10054  qextlt  12584  qextle  12585  xsubge0  12642  hashf1  13811  climuni  14901  rpnnen2lem12  15570  fzo0dvdseq  15665  4sqlem11  16281  haust1  21957  deg1lt0  24692  ply1divmo  24736  ig1peu  24772  dgrlt  24863  quotcan  24905  fta  25665  atcv0eq  30162  erdszelem9  32559  poimirlem23  35080  poimir  35090  lshpdisj  36283  lsatcv0eq  36343  exatleN  36700  atcvr0eq  36722  cdlemg31c  37995  itrere  39591  retire  39592  jm2.19  39934  jm2.26lem3  39942  dgraa0p  40093