Theorem necon4ad 2975

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

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

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 2957

This theorem is used by:  necon1d  2978  fisseneq  9238  f1finf1o  9248  dfac5  10188  isf32lem9  10420  fpwwe2  10709  qextlt  13314  qextle  13315  xsubge0  13372  hashf1  14582  climuni  15699  rpnnen2lem12  16373  fzo0dvdseq  16473  4sqlem11  17113  haust1  23650  deg1lt0  26389  ply1divmo  26434  ig1peu  26473  dgrlt  26565  quotcan  26614  fta  27389  atcv0eq  32963  erdszelem9  35933  poimirlem23  38529  poimir  38539  lshpdisj  40012  lsatcv0eq  40072  exatleN  40429  atcvr0eq  40451  cdlemg31c  41724  sn-itrere  43520  sn-retire  43521  jm2.19  43953  jm2.26lem3  43961  dgraa0p  44109