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  9259  f1finf1o  9273  f1finf1oOLD  9274  dfac5  10125  isf32lem9  10358  fpwwe2  10640  qextlt  13184  qextle  13185  xsubge0  13242  hashf1  14420  climuni  15498  rpnnen2lem12  16170  fzo0dvdseq  16268  4sqlem11  16890  haust1  22863  deg1lt0  25616  ply1divmo  25660  ig1peu  25696  dgrlt  25787  quotcan  25829  fta  26591  atcv0eq  31670  erdszelem9  34259  poimirlem23  36597  poimir  36607  lshpdisj  37943  lsatcv0eq  38003  exatleN  38361  atcvr0eq  38383  cdlemg31c  39656  itrere  41421  retire  41422  jm2.19  41814  jm2.26lem3  41822  dgraa0p  41973