Theorem necon4ad 2945

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

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

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 2927

This theorem is referenced by:  necon1d  2948  fisseneq  9211  f1finf1o  9223  f1finf1oOLD  9224  dfac5  10089  isf32lem9  10321  fpwwe2  10603  qextlt  13170  qextle  13171  xsubge0  13228  hashf1  14429  climuni  15525  rpnnen2lem12  16200  fzo0dvdseq  16300  4sqlem11  16933  haust1  23246  deg1lt0  26003  ply1divmo  26048  ig1peu  26087  dgrlt  26179  quotcan  26224  fta  26997  atcv0eq  32315  erdszelem9  35193  poimirlem23  37644  poimir  37654  lshpdisj  38987  lsatcv0eq  39047  exatleN  39405  atcvr0eq  39427  cdlemg31c  40700  sn-itrere  42483  sn-retire  42484  jm2.19  42989  jm2.26lem3  42997  dgraa0p  43145