Theorem necon4ad 2965

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon1d  2968  fisseneq  9320  f1finf1o  9333  f1finf1oOLD  9334  dfac5  10198  isf32lem9  10430  fpwwe2  10712  qextlt  13265  qextle  13266  xsubge0  13323  hashf1  14506  climuni  15598  rpnnen2lem12  16273  fzo0dvdseq  16371  4sqlem11  17002  haust1  23381  deg1lt0  26150  ply1divmo  26195  ig1peu  26234  dgrlt  26326  quotcan  26369  fta  27141  atcv0eq  32411  erdszelem9  35167  poimirlem23  37603  poimir  37613  lshpdisj  38943  lsatcv0eq  39003  exatleN  39361  atcvr0eq  39383  cdlemg31c  40656  itrere  42307  sn-itrere  42444  sn-retire  42445  jm2.19  42950  jm2.26lem3  42958  dgraa0p  43106