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

Theorem sylibd 217
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 210 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 45 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  3imtr3d  270  ceqsalt  3104  sbceqal  3351  csbiebt  3415  rspcsbela  3823  elrnrexdm  6038  isoselem  6244  riotass2  6290  ordzsl  6683  oaword2  7259  oaordex  7264  omword1  7279  om00  7281  omeulem2  7289  oen0  7292  oeeui  7308  nnaordex  7344  php3  7761  onomeneq  7765  frfi  7819  infglb  8009  suc11reg  8127  cardne  8401  cardsdomel  8410  carduni  8417  acndom  8483  alephinit  8527  cfflb  8690  cfslb2n  8699  fin23lem28  8771  isf34lem6  8811  fin1a2lem9  8839  axcc3  8869  winalim2  9122  inar1  9201  rankcf  9203  addclprlem2  9443  mulclprlem  9445  ltexprlem7  9468  prlem936  9473  reclem4pr  9476  sqgt0sr  9531  ltord2  10144  leord2  10145  eqord2  10146  mulgt1  10465  mulge0b  10476  fiminre  10556  lt2halves  10848  addltmul  10849  zextlt  11011  recnz  11012  zeo  11022  peano5uzi  11025  uzm1  11190  irradd  11289  irrmul  11290  xltneg  11511  xleadd1  11542  xmulasslem  11572  xlemul1a  11575  xlemul1  11577  fznuz  11877  uznfz  11878  axdc4uzlem  12195  facndiv  12473  hashvnfin  12541  hashgt12el  12593  hashgt12el2  12594  hashf1  12618  swrdccatin2  12834  swrdccatin2d  12847  swrdccatin12d  12848  rennim  13291  cau3lem  13406  caubnd2  13409  o1lo1  13589  climrlim2  13599  climshft  13628  subcn2  13646  mulcn2  13647  rlimo1  13668  o1dif  13681  isercoll  13719  caucvgrlem  13724  caucvgrlemOLD  13725  serf0  13735  cvgrat  13927  efieq1re  14241  moddvds  14300  dvdseq  14340  smuval2  14444  nn0seqcvgd  14517  algcvgblem  14524  eucalglt  14532  lcmgcdlem  14559  coprmdvds  14647  isprm6  14654  rpexp  14660  rpmul  14663  eulerthlem2  14718  prmdiv  14721  pcprendvds2  14779  pcz  14818  pcprmpw  14820  pcadd2  14823  pcfac  14832  expnprm  14835  ramlb  14965  prmgaplcmlem1OLD  15000  firest  15319  joineu  16244  meeteu  16258  latjlej1  16299  latjlej2  16300  latmlem1  16315  latmlem2  16316  lubun  16357  acsmapd  16412  imasgrp2  16789  issubg4  16824  psgnunilem4  17126  oddvdsnn0  17181  odmulgeq  17196  subgpgp  17237  odcau  17244  lsmlub  17303  frgpnabllem1  17497  pgpfac1lem2  17696  pgpfac1lem3a  17697  pgpfac1lem3  17698  irredrmul  17923  islmhm2  18249  lsmelval2  18296  lspsnat  18356  znidomb  19119  ip2eq  19207  lsmcss  19242  cnpnei  20267  cncls2  20276  cncls  20277  cnntr  20278  cnt0  20349  isnrm2  20361  comppfsc  20534  kqcldsat  20735  isr0  20739  hmeoopn  20768  hmeocld  20769  trufil  20912  opnsubg  21109  ghmcnp  21116  tgphaus  21118  qustgpopn  21121  tsmsgsum  21140  isngp4  21612  xrhmeo  21961  bndth  21973  cfilres  22253  caubl  22264  ivthlem2  22390  ovolicc2  22463  ismbf3d  22597  itg1ge0a  22656  mbfi1flim  22668  itg2gt0  22705  dvge0  22945  dvcnvrelem1  22956  dvcvx  22959  mdegmullem  23014  ig1peu  23109  ig1peuOLD  23110  plyco  23182  coemulc  23196  dgreq0  23206  dgrlt  23207  plymul0or  23221  plydiveu  23238  quotcan  23249  aalioulem3  23277  ulmcaulem  23336  sincosq3sgn  23442  sincosq4sgn  23443  sineq0  23463  logrec  23687  xrlimcnp  23881  cxploglim  23890  lgamgulmlem1  23941  sgmss  24020  mumul  24095  chtub  24127  perfect1  24143  dchrelbas3  24153  lgsdir2lem4  24241  lgsne0  24248  lgsquad2lem2  24274  2sqlem8a  24286  2sqblem  24292  axcontlem2  24982  cusgrarn  25173  redwlk  25322  wlkdvspth  25324  wlkiswwlk1  25404  wlklniswwlkn1  25413  clwwlkext2edg  25516  wwlksubclwwlk  25518  clwlkf1clwwlklem  25563  frgrawopreg1  25764  frgrawopreg2  25765  extwwlkfablem2  25792  rngosn3  26140  blocnilem  26431  ip2eqi  26484  ubthlem2  26499  hial0  26741  hial02  26742  hial2eq  26745  h1datomi  27220  sumspansn  27288  lnopcnbd  27675  riesz4i  27702  bra11  27747  pjss2coi  27803  pjnormssi  27807  pjorthcoi  27808  pjclem4a  27837  pj3lem1  27845  pj3cor1i  27848  hst1h  27866  stm1i  27882  strlem1  27889  golem2  27911  mdbr2  27935  dmdbr5  27947  mdsl2i  27961  atexch  28020  atcvatlem  28024  chirredlem1  28029  cdjreui  28071  cdj1i  28072  cdj3lem1  28073  xraddge02  28330  submarchi  28498  isarchiofld  28576  esumcvg  28903  bnj1468  29653  erdsze2lem2  29923  ghomf1olem  30308  btwnexch  30785  btwncolinear2  30830  btwncolinear3  30831  btwncolinear4  30832  btwncolinear5  30833  btwncolinear6  30834  nn0prpw  30972  cldbnd  30975  onsuct0  31094  onint1  31102  bj-ceqsalt0  31440  bj-ceqsalt1  31441  bj-inftyexpiinj  31603  bj-bary1lem1  31668  bj-bary1  31669  relowlssretop  31707  ltflcei  31847  tan2h  31851  poimirlem26  31880  poimirlem31  31885  ftc1anclem6  31936  dvasin  31942  dvacos  31943  fdc  31988  caushft  32004  heibor1lem  32055  bfplem2  32069  rrncmslem  32078  mpt2bi123f  32320  riotasv3d  32451  lsatcv1  32533  lub0N  32674  glb0N  32678  oplecon3b  32685  cmtbr4N  32740  cvrnbtwn2  32760  atnlt  32798  atlatle  32805  cvlsupr2  32828  cvrexchlem  32903  cvratlem  32905  atcvrj0  32912  cvrat4  32927  cvrat42  32928  4noncolr3  32937  ps-1  32961  llnnlt  33007  lplnnlt  33049  lvolnltN  33102  dalempnes  33135  dalemqnet  33136  dalem-cly  33155  dalem44  33200  pmaple  33245  cdlemblem  33277  paddss  33329  2polcon4bN  33402  ltrneq2  33632  cdlemc3  33678  cdleme11h  33751  cdleme16b  33764  cdlemednpq  33784  tendospcanN  34510  dihmeetlem13N  34806  mapdordlem2  35124  mapdn0  35156  ctbnfien  35580  rmxypairf1o  35679  monotoddzzfi  35710  oddcomabszz  35712  acongtr  35748  frege124d  36213  expgrowth  36542  sbcbi  36758  csbeq2gOLD  36774  funressnfv  38342  iccpartnel  38464  2elfz2melfz  38747  uzlidlring  39201  ply1mulgsumlem2  39453  fllog2  39653  dignn0flhalflem1  39700
  Copyright terms: Public domain W3C validator