Theorem necon4ad 3033

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1531   ≠ wne 3014

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 209  df-ne 3015

This theorem is referenced by:  necon1d  3036  fisseneq  8721  f1finf1o  8737  dfac5  9546  isf32lem9  9775  fpwwe2  10057  qextlt  12588  qextle  12589  xsubge0  12646  hashf1  13807  climuni  14901  rpnnen2lem12  15570  fzo0dvdseq  15665  4sqlem11  16283  haust1  21952  deg1lt0  24677  ply1divmo  24721  ig1peu  24757  dgrlt  24848  quotcan  24890  fta  25649  atcv0eq  30148  erdszelem9  32439  poimirlem23  34907  poimir  34917  lshpdisj  36115  lsatcv0eq  36175  exatleN  36532  atcvr0eq  36554  cdlemg31c  37827  jm2.19  39581  jm2.26lem3  39589  dgraa0p  39740