MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylibd Structured version   Unicode version

Theorem sylibd 207
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylibd.1  |-  ( ph  ->  ( ps  ->  ch ) )
sylibd.2  |-  ( ph  ->  ( ch  <->  th )
)
Assertion
Ref Expression
sylibd  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem sylibd
StepHypRef Expression
1 sylibd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylibd.2 . . 3  |-  ( ph  ->  ( ch  <->  th )
)
32biimpd 200 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 43 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  3imtr3d  260  ceqsalt  2979  sbceqal  3213  sbcimdv  3223  csbiebt  3288  rspcsbela  3309  copsexg  4443  ordzsl  4826  elrnrexdm  5875  isoselem  6062  riotass2  6578  riotasv3d  6599  riotasv3dOLD  6600  oaword2  6797  oaordex  6802  omword1  6817  om00  6819  omeulem2  6827  oen0  6830  oeeui  6846  nnaordex  6882  php3  7294  onomeneq  7297  frfi  7353  suc11reg  7575  cardne  7853  cardsdomel  7862  carduni  7869  acndom  7933  alephinit  7977  cfflb  8140  cfslb2n  8149  fin23lem28  8221  isf34lem6  8261  fin1a2lem9  8289  axcc3  8319  winalim2  8572  inar1  8651  rankcf  8653  addclprlem2  8895  mulclprlem  8897  ltexprlem7  8920  prlem936  8925  reclem4pr  8928  sqgt0sr  8982  ltord2  9557  leord2  9558  eqord2  9559  mulgt1  9870  lt2halves  10203  addltmul  10204  zextlt  10345  recnz  10346  zeo  10356  peano5uzi  10359  uzindOLD  10365  uzm1  10517  irradd  10599  irrmul  10600  xltneg  10804  xleadd1  10835  xmulasslem  10865  xlemul1a  10868  xlemul1  10870  fznuz  11130  uznfz  11131  axdc4uzlem  11322  facndiv  11580  hashvnfin  11643  hashgt12el  11683  hashgt12el2  11684  hashf1  11707  rennim  12045  cau3lem  12159  caubnd2  12162  o1lo1  12332  climrlim2  12342  climshft  12371  subcn2  12389  mulcn2  12390  rlimo1  12411  o1dif  12424  isercoll  12462  caucvgrlem  12467  serf0  12475  cvgrat  12661  efieq1re  12801  moddvds  12860  dvdseq  12898  smuval2  12995  nn0seqcvgd  13062  algcvgblem  13069  eucalglt  13077  coprmdvds  13103  isprm6  13110  rpexp  13121  rpmul  13124  eulerthlem2  13172  prmdiv  13175  pcprendvds2  13216  pcz  13255  pcprmpw  13257  pcadd2  13260  pcfac  13269  expnprm  13272  ramlb  13388  firest  13661  latjlej1  14495  latjlej2  14496  latmlem1  14511  latmlem2  14512  lubun  14551  acsmapd  14605  imasgrp2  14934  issubg4  14962  oddvdsnn0  15183  odmulgeq  15194  subgpgp  15232  odcau  15239  lsmlub  15298  frgpnabllem1  15485  pgpfac1lem2  15634  pgpfac1lem3a  15635  pgpfac1lem3  15636  irredrmul  15813  islmhm2  16115  lsmelval2  16158  lspsnat  16218  znidomb  16843  ip2eq  16885  lsmcss  16920  cnpnei  17329  cncls2  17338  cncls  17339  cnntr  17340  cnt0  17411  isnrm2  17423  kqcldsat  17766  isr0  17770  hmeoopn  17799  hmeocld  17800  trufil  17943  opnsubg  18138  ghmcnp  18145  tgphaus  18147  divstgpopn  18150  tsmsgsum  18169  isngp4  18659  xrhmeo  18972  bndth  18984  cfilres  19250  caubl  19261  ivthlem2  19350  ovolicc2  19419  ismbf3d  19547  itg1ge0a  19604  mbfi1flim  19616  itg2gt0  19653  dvge0  19891  dvcnvrelem1  19902  dvcvx  19905  mdegmullem  20002  ig1peu  20095  plyco  20161  coemulc  20174  dgreq0  20184  dgrlt  20185  plymul0or  20199  plydiveu  20216  quotcan  20227  aalioulem3  20252  ulmcaulem  20311  sincosq3sgn  20409  sincosq4sgn  20410  sineq0  20430  logrec  20662  xrlimcnp  20808  cxploglim  20817  sgmss  20890  mumul  20965  chtub  20997  perfect1  21013  dchrelbas3  21023  lgsdir2lem4  21111  lgsne0  21118  lgsquad2lem2  21144  2sqlem8a  21156  2sqblem  21162  cusgrarn  21469  redwlk  21607  wlkdvspth  21609  rngosn3  22015  blocnilem  22306  ip2eqi  22359  ubthlem2  22374  hial0  22605  hial02  22606  hial2eq  22609  h1datomi  23084  sumspansn  23152  lnopcnbd  23540  riesz4i  23567  bra11  23612  pjss2coi  23668  pjnormssi  23672  pjorthcoi  23673  pjclem4a  23702  pj3lem1  23710  pj3cor1i  23713  hst1h  23731  stm1i  23747  strlem1  23754  golem2  23776  mdbr2  23800  dmdbr5  23812  mdsl2i  23826  atexch  23885  atcvatlem  23889  chirredlem1  23894  cdjreui  23936  cdj1i  23937  cdj3lem1  23938  xraddge02  24124  esumcvg  24477  lgamgulmlem1  24814  erdsze2lem2  24891  ghomf1olem  25106  mulge0b  25192  axcontlem2  25905  btwnexch  25960  btwncolinear2  26005  btwncolinear3  26006  btwncolinear4  26007  btwncolinear5  26008  btwncolinear6  26009  onsuct0  26192  onint1  26200  ltflcei  26240  ftc1anclem6  26286  dvreasin  26291  nn0prpw  26327  cldbnd  26330  comppfsc  26388  fdc  26450  caushft  26468  heibor1lem  26519  bfplem2  26533  rrncmslem  26542  ctbnfien  26880  rmxypairf1o  26975  monotoddzzfi  27006  oddcomabszz  27008  acongtr  27044  psgnunilem4  27398  expgrowth  27530  funressnfv  27969  2elfz2melfz  28118  swrdccatin2  28211  swrdccatin2d  28222  swrdccatin12d  28223  frgrawopreg1  28440  frgrawopreg2  28441  sbcbi  28625  csbeq2g  28637  bnj1468  29218  lubunNEW  29772  lsatcv1  29847  lub0N  29988  glb0N  29992  oplecon3b  29999  cmtbr4N  30054  cvrnbtwn2  30074  atnlt  30112  atlatle  30119  cvlsupr2  30142  cvrexchlem  30217  cvratlem  30219  atcvrj0  30226  cvrat4  30241  cvrat42  30242  4noncolr3  30251  ps-1  30275  llnnlt  30321  lplnnlt  30363  lvolnltN  30416  dalempnes  30449  dalemqnet  30450  dalem-cly  30469  dalem44  30514  pmaple  30559  cdlemblem  30591  paddss  30643  2polcon4bN  30716  ltrneq2  30946  cdlemc3  30991  cdleme11h  31064  cdleme16b  31077  cdlemednpq  31097  tendospcanN  31822  dihmeetlem13N  32118  mapdordlem2  32436  mapdn0  32468
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator