Theorem necon4ad 2944

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon1d  2947  fisseneq  9204  f1finf1o  9216  f1finf1oOLD  9217  dfac5  10082  isf32lem9  10314  fpwwe2  10596  qextlt  13163  qextle  13164  xsubge0  13221  hashf1  14422  climuni  15518  rpnnen2lem12  16193  fzo0dvdseq  16293  4sqlem11  16926  haust1  23239  deg1lt0  25996  ply1divmo  26041  ig1peu  26080  dgrlt  26172  quotcan  26217  fta  26990  atcv0eq  32308  erdszelem9  35186  poimirlem23  37637  poimir  37647  lshpdisj  38980  lsatcv0eq  39040  exatleN  39398  atcvr0eq  39420  cdlemg31c  40693  sn-itrere  42476  sn-retire  42477  jm2.19  42982  jm2.26lem3  42990  dgraa0p  43138