Theorem necon4ad 2980

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 143	. 2 ⊢ (𝜓 → ¬ ¬ 𝜓)
2		necon4ad.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → ¬ 𝜓))
3	2	necon1bd 2979	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝐴 = 𝐵))
4	1, 3	syl5 35	1 ⊢ (𝜑 → (𝜓 → 𝐴 = 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2962

This theorem is used by:  necon1d  2983  fisseneq  9233  f1finf1o  9243  dfac5  10131  isf32lem9  10363  fpwwe2  10646  qextlt  13247  qextle  13248  xsubge0  13305  hashf1  14514  climuni  15629  rpnnen2lem12  16306  fzo0dvdseq  16406  4sqlem11  17040  haust1  23546  deg1lt0  26285  ply1divmo  26330  ig1peu  26369  dgrlt  26460  quotcan  26507  fta  27281  atcv0eq  32768  erdszelem9  35712  poimirlem23  38335  poimir  38345  lshpdisj  39802  lsatcv0eq  39862  exatleN  40219  atcvr0eq  40241  cdlemg31c  41514  sn-itrere  43303  sn-retire  43304  jm2.19  43761  jm2.26lem3  43769  dgraa0p  43917