Theorem necon4ad 2952

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

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

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 2934

This theorem is referenced by:  necon1d  2955  fisseneq  9166  f1finf1o  9176  dfac5  10042  isf32lem9  10274  fpwwe2  10557  qextlt  13146  qextle  13147  xsubge0  13204  hashf1  14410  climuni  15505  rpnnen2lem12  16183  fzo0dvdseq  16283  4sqlem11  16917  haust1  23327  deg1lt0  26066  ply1divmo  26111  ig1peu  26150  dgrlt  26241  quotcan  26286  fta  27057  atcv0eq  32465  erdszelem9  35397  poimirlem23  37978  poimir  37988  lshpdisj  39447  lsatcv0eq  39507  exatleN  39864  atcvr0eq  39886  cdlemg31c  41159  sn-itrere  42947  sn-retire  42948  jm2.19  43439  jm2.26lem3  43447  dgraa0p  43595