Theorem necon1bd 2957

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

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

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 206  df-ne 2940

This theorem is referenced by:  necon4ad  2958  fvclss  7225  suppssr  8163  suppssrg  8164  suppofssd  8170  eceqoveq  8799  fofinf1o  9310  cantnfp1lem3  9657  cantnfp1  9658  mul0or  11836  inelr  12184  rimul  12185  rlimuni  15476  pc2dvds  16794  divsfval  17475  pleval2i  18271  lssvs0or  20672  lspsnat  20707  lmmo  22813  filssufilg  23344  hausflimi  23413  fclscf  23458  xrsmopn  24257  rectbntr0  24277  bcth3  24777  limcco  25339  ig1pdvds  25623  plyco0  25635  plypf1  25655  coeeulem  25667  coeidlem  25680  coeid3  25683  coemullem  25693  coemulhi  25697  coemulc  25698  dgradd2  25711  vieta1lem2  25753  dvtaylp  25811  musum  26622  perfectlem2  26660  dchrelbas3  26668  dchrmullid  26682  dchreq  26688  dchrsum  26699  gausslemma2dlem4  26799  dchrisum0re  26943  coltr  27763  lmieu  27900  elspansn5  30690  atomli  31498  pthisspthorcycl  33950  onsucconni  35126  poimirlem8  36300  poimirlem9  36301  poimirlem18  36310  poimirlem21  36313  poimirlem22  36314  poimirlem26  36318  lshpcmp  37663  lsator0sp  37676  atnle  37992  atlatmstc  37994  osumcllem8N  38639  osumcllem11N  38642  pexmidlem5N  38650  pexmidlem8N  38653  dochsat0  40133  dochexmidlem5  40140  dochexmidlem8  40143  fsuppind  40951  congabseq  41484  dflim5  41850  mnringmulrcld  42758  perfectALTVlem2  46162