Theorem necon4ad 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon1d  2957  fisseneq  9170  f1finf1o  9180  dfac5  10049  isf32lem9  10281  fpwwe2  10564  qextlt  13153  qextle  13154  xsubge0  13211  hashf1  14417  climuni  15512  rpnnen2lem12  16190  fzo0dvdseq  16290  4sqlem11  16924  haust1  23342  deg1lt0  26081  ply1divmo  26126  ig1peu  26165  dgrlt  26256  quotcan  26300  fta  27068  atcv0eq  32475  erdszelem9  35434  poimirlem23  38017  poimir  38027  lshpdisj  39486  lsatcv0eq  39546  exatleN  39903  atcvr0eq  39925  cdlemg31c  41198  sn-itrere  42985  sn-retire  42986  jm2.19  43445  jm2.26lem3  43453  dgraa0p  43601