Theorem necon4ad 2948

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  necon1d  2951  fisseneq  9154  f1finf1o  9164  dfac5  10027  isf32lem9  10259  fpwwe2  10541  qextlt  13104  qextle  13105  xsubge0  13162  hashf1  14366  climuni  15461  rpnnen2lem12  16136  fzo0dvdseq  16236  4sqlem11  16869  haust1  23268  deg1lt0  26024  ply1divmo  26069  ig1peu  26108  dgrlt  26200  quotcan  26245  fta  27018  atcv0eq  32361  erdszelem9  35264  poimirlem23  37703  poimir  37713  lshpdisj  39106  lsatcv0eq  39166  exatleN  39523  atcvr0eq  39545  cdlemg31c  40818  sn-itrere  42606  sn-retire  42607  jm2.19  43110  jm2.26lem3  43118  dgraa0p  43266