MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon1bd Structured version   Visualization version   GIF version

Theorem necon1bd 2958
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
StepHypRef Expression
1 df-ne 2941 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon1bd.1 . . 3 (𝜑 → (𝐴𝐵𝜓))
31, 2biimtrrid 242 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝜓))
43con1d 145 1 (𝜑 → (¬ 𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2940
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 2941
This theorem is referenced by:  necon4ad  2959  fvclss  7193  suppssr  8131  suppssrg  8132  suppofssd  8138  eceqoveq  8767  fofinf1o  9277  cantnfp1lem3  9624  cantnfp1  9625  mul0or  11803  inelr  12151  rimul  12152  rlimuni  15441  pc2dvds  16759  divsfval  17437  pleval2i  18233  lssvs0or  20616  lspsnat  20651  lmmo  22754  filssufilg  23285  hausflimi  23354  fclscf  23399  xrsmopn  24198  rectbntr0  24218  bcth3  24718  limcco  25280  ig1pdvds  25564  plyco0  25576  plypf1  25596  coeeulem  25608  coeidlem  25621  coeid3  25624  coemullem  25634  coemulhi  25638  coemulc  25639  dgradd2  25652  vieta1lem2  25694  dvtaylp  25752  musum  26563  perfectlem2  26601  dchrelbas3  26609  dchrmulid2  26623  dchreq  26629  dchrsum  26640  gausslemma2dlem4  26740  dchrisum0re  26884  coltr  27638  lmieu  27775  elspansn5  30565  atomli  31373  pthisspthorcycl  33786  onsucconni  34962  poimirlem8  36136  poimirlem9  36137  poimirlem18  36146  poimirlem21  36149  poimirlem22  36150  poimirlem26  36154  lshpcmp  37500  lsator0sp  37513  atnle  37829  atlatmstc  37831  osumcllem8N  38476  osumcllem11N  38479  pexmidlem5N  38487  pexmidlem8N  38490  dochsat0  39970  dochexmidlem5  39977  dochexmidlem8  39980  fsuppind  40812  congabseq  41345  dflim5  41711  mnringmulrcld  42600  perfectALTVlem2  46004
  Copyright terms: Public domain W3C validator