Theorem necon4ad 2959

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

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

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 206  df-ne 2941

This theorem is referenced by:  necon1d  2962  fisseneq  9256  f1finf1o  9270  f1finf1oOLD  9271  dfac5  10122  isf32lem9  10355  fpwwe2  10637  qextlt  13181  qextle  13182  xsubge0  13239  hashf1  14417  climuni  15495  rpnnen2lem12  16167  fzo0dvdseq  16265  4sqlem11  16887  haust1  22855  deg1lt0  25608  ply1divmo  25652  ig1peu  25688  dgrlt  25779  quotcan  25821  fta  26581  atcv0eq  31627  erdszelem9  34185  poimirlem23  36506  poimir  36516  lshpdisj  37852  lsatcv0eq  37912  exatleN  38270  atcvr0eq  38292  cdlemg31c  39565  itrere  41340  retire  41341  jm2.19  41722  jm2.26lem3  41730  dgraa0p  41881