Theorem necon4ad 2975

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

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

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 2957

This theorem is used by:  necon1d  2978  fisseneq  9254  f1finf1o  9264  dfac5  10207  isf32lem9  10439  fpwwe2  10728  qextlt  13333  qextle  13334  xsubge0  13391  hashf1  14602  climuni  15719  rpnnen2lem12  16393  fzo0dvdseq  16493  4sqlem11  17133  haust1  23670  deg1lt0  26409  ply1divmo  26454  ig1peu  26493  dgrlt  26585  quotcan  26632  fta  27407  atcv0eq  32981  erdszelem9  35964  poimirlem23  38562  poimir  38572  lshpdisj  40045  lsatcv0eq  40105  exatleN  40462  atcvr0eq  40484  cdlemg31c  41757  sn-itrere  43553  sn-retire  43554  jm2.19  44000  jm2.26lem3  44008  dgraa0p  44151