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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631   ≠ 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 197  df-ne 2944

This theorem is referenced by:  necon1d  2965  fisseneq  8331  f1finf1o  8347  dfac5  9155  isf32lem9  9389  fpwwe2  9671  qextlt  12239  qextle  12240  xsubge0  12296  hashf1  13443  climuni  14491  rpnnen2lem12  15160  fzo0dvdseq  15254  4sqlem11  15866  haust1  21377  deg1lt0  24071  ply1divmo  24115  ig1peu  24151  dgrlt  24242  quotcan  24284  fta  25027  atcv0eq  29578  erdszelem9  31519  poimirlem23  33765  poimir  33775  lshpdisj  34796  lsatcv0eq  34856  exatleN  35213  atcvr0eq  35235  cdlemg31c  36509  jm2.19  38086  jm2.26lem3  38094  dgraa0p  38245