Theorem necon1bd 2955

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 2938	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bd.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
3	1, 2	biimtrrid 243	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓))
4	3	con1d 145	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  necon4ad  2956  fvclss  7260  suppssr  8218  suppssrg  8219  suppofssd  8226  eceqoveq  8860  fofinf1o  9369  cantnfp1lem3  9717  cantnfp1  9718  mul0or  11900  inelr  12253  rimul  12254  rlimuni  15582  pc2dvds  16912  divsfval  17593  pleval2i  18393  lssvs0or  21129  lspsnat  21164  psdmul  22187  lmmo  23403  filssufilg  23934  hausflimi  24003  fclscf  24048  xrsmopn  24847  rectbntr0  24867  bcth3  25378  limcco  25942  ig1pdvds  26233  plyco0  26245  plypf1  26265  coeeulem  26277  coeidlem  26290  coeid3  26293  coemullem  26303  coemulhi  26307  coemulc  26308  dgradd2  26322  vieta1lem2  26367  dvtaylp  26426  musum  27248  perfectlem2  27288  dchrelbas3  27296  dchrmullid  27310  dchreq  27316  dchrsum  27327  gausslemma2dlem4  27427  dchrisum0re  27571  muls0ord  28225  coltr  28669  lmieu  28806  elspansn5  31602  atomli  32410  pthisspthorcycl  35112  onsucconni  36419  poimirlem8  37614  poimirlem9  37615  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem26  37632  lshpcmp  38969  lsator0sp  38982  atnle  39298  atlatmstc  39300  osumcllem8N  39945  osumcllem11N  39948  pexmidlem5N  39956  pexmidlem8N  39959  dochsat0  41439  dochexmidlem5  41446  dochexmidlem8  41449  aks6d1c4  42105  fsuppind  42576  congabseq  42962  dflim5  43318  mnringmulrcld  44223  perfectALTVlem2  47646