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

Theorem necon1bd 3034
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 3017 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon1bd.1 . . 3 (𝜑 → (𝐴𝐵𝜓))
31, 2syl5bir 244 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝜓))
43con1d 147 1 (𝜑 → (¬ 𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  necon4ad  3035  fvclss  6992  suppssr  7852  suppofssd  7858  eceqoveq  8392  fofinf1o  8788  cantnfp1lem3  9132  cantnfp1  9133  mul0or  11269  inelr  11617  rimul  11618  rlimuni  14897  pc2dvds  16205  divsfval  16810  pleval2i  17564  lssvs0or  19813  lspsnat  19848  lmmo  21918  filssufilg  22449  hausflimi  22518  fclscf  22563  xrsmopn  23349  rectbntr0  23369  bcth3  23863  limcco  24420  ig1pdvds  24699  plyco0  24711  plypf1  24731  coeeulem  24743  coeidlem  24756  coeid3  24759  coemullem  24769  coemulhi  24773  coemulc  24774  dgradd2  24787  vieta1lem2  24829  dvtaylp  24887  musum  25696  perfectlem2  25734  dchrelbas3  25742  dchrmulid2  25756  dchreq  25762  dchrsum  25773  gausslemma2dlem4  25873  dchrisum0re  26017  coltr  26361  lmieu  26498  elspansn5  29279  atomli  30087  pthisspthorcycl  32273  onsucconni  33683  poimirlem8  34782  poimirlem9  34783  poimirlem18  34792  poimirlem21  34795  poimirlem22  34796  poimirlem26  34800  lshpcmp  36006  lsator0sp  36019  atnle  36335  atlatmstc  36337  osumcllem8N  36981  osumcllem11N  36984  pexmidlem5N  36992  pexmidlem8N  36995  dochsat0  38475  dochexmidlem5  38482  dochexmidlem8  38485  congabseq  39451  perfectALTVlem2  43734
  Copyright terms: Public domain W3C validator