Theorem necon4ad 2952

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2933

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 2934

This theorem is referenced by:  necon1d  2955  fisseneq  9270  f1finf1o  9282  f1finf1oOLD  9283  dfac5  10148  isf32lem9  10380  fpwwe2  10662  qextlt  13224  qextle  13225  xsubge0  13282  hashf1  14480  climuni  15573  rpnnen2lem12  16248  fzo0dvdseq  16347  4sqlem11  16980  haust1  23295  deg1lt0  26053  ply1divmo  26098  ig1peu  26137  dgrlt  26229  quotcan  26274  fta  27047  atcv0eq  32365  erdszelem9  35226  poimirlem23  37672  poimir  37682  lshpdisj  39010  lsatcv0eq  39070  exatleN  39428  atcvr0eq  39450  cdlemg31c  40723  itrere  42334  sn-itrere  42478  sn-retire  42479  jm2.19  42984  jm2.26lem3  42992  dgraa0p  43140