Theorem necon4ad 2951

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  necon1d  2954  fisseneq  9173  f1finf1o  9183  dfac5  10051  isf32lem9  10283  fpwwe2  10566  qextlt  13155  qextle  13156  xsubge0  13213  hashf1  14419  climuni  15514  rpnnen2lem12  16192  fzo0dvdseq  16292  4sqlem11  16926  haust1  23317  deg1lt0  26056  ply1divmo  26101  ig1peu  26140  dgrlt  26231  quotcan  26275  fta  27043  atcv0eq  32450  erdszelem9  35381  poimirlem23  37964  poimir  37974  lshpdisj  39433  lsatcv0eq  39493  exatleN  39850  atcvr0eq  39872  cdlemg31c  41145  sn-itrere  42933  sn-retire  42934  jm2.19  43421  jm2.26lem3  43429  dgraa0p  43577