Theorem necon4ad 2990

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1653   ≠ wne 2971

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 199  df-ne 2972

This theorem is referenced by:  necon1d  2993  fisseneq  8413  f1finf1o  8429  dfac5  9237  isf32lem9  9471  fpwwe2  9753  qextlt  12283  qextle  12284  xsubge0  12340  hashf1  13490  climuni  14624  rpnnen2lem12  15290  fzo0dvdseq  15384  4sqlem11  15992  haust1  21485  deg1lt0  24192  ply1divmo  24236  ig1peu  24272  dgrlt  24363  quotcan  24405  fta  25158  atcv0eq  29763  erdszelem9  31698  poimirlem23  33921  poimir  33931  lshpdisj  35008  lsatcv0eq  35068  exatleN  35425  atcvr0eq  35447  cdlemg31c  36720  jm2.19  38345  jm2.26lem3  38353  dgraa0p  38504