Theorem necon4ad 2947

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  necon1d  2950  fisseneq  9147  f1finf1o  9157  dfac5  10017  isf32lem9  10249  fpwwe2  10531  qextlt  13099  qextle  13100  xsubge0  13157  hashf1  14361  climuni  15456  rpnnen2lem12  16131  fzo0dvdseq  16231  4sqlem11  16864  haust1  23265  deg1lt0  26021  ply1divmo  26066  ig1peu  26105  dgrlt  26197  quotcan  26242  fta  27015  atcv0eq  32354  erdszelem9  35231  poimirlem23  37682  poimir  37692  lshpdisj  39025  lsatcv0eq  39085  exatleN  39442  atcvr0eq  39464  cdlemg31c  40737  sn-itrere  42520  sn-retire  42521  jm2.19  43025  jm2.26lem3  43033  dgraa0p  43181