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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necon1d  2978  fisseneq  9203  f1finf1o  9213  dfac5  10082  isf32lem9  10315  fpwwe2  10598  qextlt  13203  qextle  13204  xsubge0  13261  hashf1  14467  climuni  15562  rpnnen2lem12  16240  fzo0dvdseq  16340  4sqlem11  16974  haust1  23392  deg1lt0  26131  ply1divmo  26176  ig1peu  26215  dgrlt  26306  quotcan  26350  fta  27121  atcv0eq  32528  erdszelem9  35513  poimirlem23  38106  poimir  38116  lshpdisj  39575  lsatcv0eq  39635  exatleN  39992  atcvr0eq  40014  cdlemg31c  41287  sn-itrere  43074  sn-retire  43075  jm2.19  43534  jm2.26lem3  43542  dgraa0p  43690