Theorem necon4ad 2801

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon1d  2804  fisseneq  8056  f1finf1o  8072  dfac5  8834  isf32lem9  9066  fpwwe2  9344  qextlt  11908  qextle  11909  xsubge0  11963  hashf1  13098  climuni  14131  rpnnen2lem12  14793  fzo0dvdseq  14883  4sqlem11  15497  haust1  20966  deg1lt0  23655  ply1divmo  23699  ig1peu  23735  dgrlt  23826  quotcan  23868  fta  24606  atcv0eq  28622  erdszelem9  30435  poimirlem23  32602  poimir  32612  lshpdisj  33292  lsatcv0eq  33352  exatleN  33708  atcvr0eq  33730  cdlemg31c  35005  jm2.19  36578  jm2.26lem3  36586  dgraa0p  36738