Theorem necon4ad 2978

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

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

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 2960

This theorem is used by:  necon1d  2981  fisseneq  9282  f1finf1o  9292  dfac5  10234  isf32lem9  10466  fpwwe2  10755  qextlt  13360  qextle  13361  xsubge0  13418  hashf1  14629  climuni  15748  rpnnen2lem12  16422  fzo0dvdseq  16522  4sqlem11  17162  haust1  23700  deg1lt0  26439  ply1divmo  26484  ig1peu  26523  dgrlt  26615  quotcan  26662  fta  27437  atcv0eq  33011  erdszelem9  36131  poimirlem23  38753  poimir  38763  lshpdisj  40236  lsatcv0eq  40296  exatleN  40653  atcvr0eq  40675  cdlemg31c  41948  sn-itrere  43745  sn-retire  43746  jm2.19  44193  jm2.26lem3  44201  dgraa0p  44343