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  9175  f1finf1o  9185  dfac5  10051  isf32lem9  10283  fpwwe2  10566  qextlt  13130  qextle  13131  xsubge0  13188  hashf1  14392  climuni  15487  rpnnen2lem12  16162  fzo0dvdseq  16262  4sqlem11  16895  haust1  23308  deg1lt0  26064  ply1divmo  26109  ig1peu  26148  dgrlt  26240  quotcan  26285  fta  27058  atcv0eq  32466  erdszelem9  35412  poimirlem23  37888  poimir  37898  lshpdisj  39357  lsatcv0eq  39417  exatleN  39774  atcvr0eq  39796  cdlemg31c  41069  sn-itrere  42852  sn-retire  42853  jm2.19  43344  jm2.26lem3  43352  dgraa0p  43500