Theorem necon1bd 2944

Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypothesis

Ref	Expression
necon1bd.1	⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))

Assertion

Ref	Expression
necon1bd	⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

Proof of Theorem necon1bd

Step	Hyp	Ref	Expression
1		df-ne 2927	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bd.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
3	1, 2	biimtrrid 243	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓))
4	3	con1d 145	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

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

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 2927

This theorem is referenced by:  necon4ad  2945  fvclss  7218  suppssr  8177  suppssrg  8178  suppofssd  8185  eceqoveq  8798  fofinf1o  9290  cantnfp1lem3  9640  cantnfp1  9641  mul0or  11825  rimul  12184  rlimuni  15523  pc2dvds  16857  divsfval  17517  pleval2i  18302  lssvs0or  21027  lspsnat  21062  psdmul  22060  lmmo  23274  filssufilg  23805  hausflimi  23874  fclscf  23919  xrsmopn  24708  rectbntr0  24728  bcth3  25238  limcco  25801  ig1pdvds  26092  plyco0  26104  plypf1  26124  coeeulem  26136  coeidlem  26149  coeid3  26152  coemullem  26162  coemulhi  26166  coemulc  26167  dgradd2  26181  vieta1lem2  26226  dvtaylp  26285  musum  27108  perfectlem2  27148  dchrelbas3  27156  dchrmullid  27170  dchreq  27176  dchrsum  27187  gausslemma2dlem4  27287  dchrisum0re  27431  muls0ord  28095  coltr  28581  lmieu  28718  pthisspthorcycl  29739  elspansn5  31510  atomli  32318  onsucconni  36432  poimirlem8  37629  poimirlem9  37630  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  poimirlem26  37647  lshpcmp  38988  lsator0sp  39001  atnle  39317  atlatmstc  39319  osumcllem8N  39964  osumcllem11N  39967  pexmidlem5N  39975  pexmidlem8N  39978  dochsat0  41458  dochexmidlem5  41465  dochexmidlem8  41468  aks6d1c4  42119  sn-remul0ord  42403  fsuppind  42585  congabseq  42970  dflim5  43325  mnringmulrcld  44224  perfectALTVlem2  47727