Theorem necon1bd 2950

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  necon4ad  2951  fvclss  7187  suppssr  8137  suppssrg  8138  suppofssd  8145  eceqoveq  8759  fofinf1o  9232  cantnfp1lem3  9589  cantnfp1  9590  mul0or  11777  rimul  12136  rlimuni  15473  pc2dvds  16807  divsfval  17468  pleval2i  18257  lssvs0or  21065  lspsnat  21100  psdmul  22109  lmmo  23324  filssufilg  23855  hausflimi  23924  fclscf  23969  xrsmopn  24757  rectbntr0  24777  bcth3  25287  limcco  25850  ig1pdvds  26141  plyco0  26153  plypf1  26173  coeeulem  26185  coeidlem  26198  coeid3  26201  coemullem  26211  coemulhi  26215  coemulc  26216  dgradd2  26230  vieta1lem2  26275  dvtaylp  26334  musum  27157  perfectlem2  27197  dchrelbas3  27205  dchrmullid  27219  dchreq  27225  dchrsum  27236  gausslemma2dlem4  27336  dchrisum0re  27480  muls0ord  28181  coltr  28719  lmieu  28856  pthisspthorcycl  29875  elspansn5  31649  atomli  32457  onsucconni  36631  poimirlem8  37829  poimirlem9  37830  poimirlem18  37839  poimirlem21  37842  poimirlem22  37843  poimirlem26  37847  lshpcmp  39248  lsator0sp  39261  atnle  39577  atlatmstc  39579  osumcllem8N  40223  osumcllem11N  40226  pexmidlem5N  40234  pexmidlem8N  40237  dochsat0  41717  dochexmidlem5  41724  dochexmidlem8  41727  aks6d1c4  42378  sn-remul0ord  42663  fsuppind  42833  congabseq  43216  dflim5  43571  mnringmulrcld  44469  perfectALTVlem2  47968