Theorem necon4ad 2974

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon1d  2977  fisseneq  9257  f1finf1o  9267  dfac5  10210  isf32lem9  10442  fpwwe2  10731  qextlt  13336  qextle  13337  xsubge0  13394  hashf1  14605  climuni  15724  rpnnen2lem12  16398  fzo0dvdseq  16498  4sqlem11  17138  haust1  23675  deg1lt0  26414  ply1divmo  26459  ig1peu  26498  dgrlt  26590  quotcan  26637  fta  27412  atcv0eq  32986  erdszelem9  36050  poimirlem23  38654  poimir  38664  lshpdisj  40137  lsatcv0eq  40197  exatleN  40554  atcvr0eq  40576  cdlemg31c  41849  sn-itrere  43645  sn-retire  43646  jm2.19  44093  jm2.26lem3  44101  dgraa0p  44244