Theorem necon4ad 2952

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  necon1d  2955  fisseneq  9167  f1finf1o  9177  dfac5  10043  isf32lem9  10275  fpwwe2  10558  qextlt  13122  qextle  13123  xsubge0  13180  hashf1  14384  climuni  15479  rpnnen2lem12  16154  fzo0dvdseq  16254  4sqlem11  16887  haust1  23300  deg1lt0  26056  ply1divmo  26101  ig1peu  26140  dgrlt  26232  quotcan  26277  fta  27050  atcv0eq  32437  erdszelem9  35374  poimirlem23  37815  poimir  37825  lshpdisj  39284  lsatcv0eq  39344  exatleN  39701  atcvr0eq  39723  cdlemg31c  40996  sn-itrere  42779  sn-retire  42780  jm2.19  43271  jm2.26lem3  43279  dgraa0p  43427