Theorem necon4ad 2813

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon1d  2816  fisseneq  8171  f1finf1o  8187  dfac5  8951  isf32lem9  9183  fpwwe2  9465  qextlt  12034  qextle  12035  xsubge0  12091  hashf1  13241  climuni  14283  rpnnen2lem12  14954  fzo0dvdseq  15045  4sqlem11  15659  haust1  21156  deg1lt0  23851  ply1divmo  23895  ig1peu  23931  dgrlt  24022  quotcan  24064  fta  24806  atcv0eq  29238  erdszelem9  31181  poimirlem23  33432  poimir  33442  lshpdisj  34274  lsatcv0eq  34334  exatleN  34690  atcvr0eq  34712  cdlemg31c  35987  jm2.19  37560  jm2.26lem3  37568  dgraa0p  37719