Theorem necon4ad 2962

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

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 206  df-ne 2944

This theorem is referenced by:  necon1d  2965  fisseneq  9034  f1finf1o  9046  dfac5  9884  isf32lem9  10117  fpwwe2  10399  qextlt  12937  qextle  12938  xsubge0  12995  hashf1  14171  climuni  15261  rpnnen2lem12  15934  fzo0dvdseq  16032  4sqlem11  16656  haust1  22503  deg1lt0  25256  ply1divmo  25300  ig1peu  25336  dgrlt  25427  quotcan  25469  fta  26229  atcv0eq  30741  erdszelem9  33161  poimirlem23  35800  poimir  35810  lshpdisj  37001  lsatcv0eq  37061  exatleN  37418  atcvr0eq  37440  cdlemg31c  38713  itrere  40436  retire  40437  jm2.19  40815  jm2.26lem3  40823  dgraa0p  40974