Theorem necon4ad 2976

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

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

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 2958

This theorem is used by:  necon1d  2979  fisseneq  9237  f1finf1o  9247  dfac5  10135  isf32lem9  10367  fpwwe2  10656  qextlt  13259  qextle  13260  xsubge0  13317  hashf1  14526  climuni  15643  rpnnen2lem12  16319  fzo0dvdseq  16419  4sqlem11  17053  haust1  23583  deg1lt0  26323  ply1divmo  26368  ig1peu  26407  dgrlt  26499  quotcan  26548  fta  27324  atcv0eq  32868  erdszelem9  35786  poimirlem23  38400  poimir  38410  lshpdisj  39868  lsatcv0eq  39928  exatleN  40285  atcvr0eq  40307  cdlemg31c  41580  sn-itrere  43384  sn-retire  43385  jm2.19  43842  jm2.26lem3  43850  dgraa0p  43998