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

Theorem sylibd 214
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 207 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 44 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  3imtr3d  267  ceqsalt  3129  sbceqal  3376  csbiebt  3440  rspcsbela  3845  elrnrexdm  6011  isoselem  6212  riotass2  6258  ordzsl  6653  oaword2  7194  oaordex  7199  omword1  7214  om00  7216  omeulem2  7224  oen0  7227  oeeui  7243  nnaordex  7279  php3  7696  onomeneq  7700  frfi  7757  suc11reg  8027  cardne  8337  cardsdomel  8346  carduni  8353  acndom  8423  alephinit  8467  cfflb  8630  cfslb2n  8639  fin23lem28  8711  isf34lem6  8751  fin1a2lem9  8779  axcc3  8809  winalim2  9063  inar1  9142  rankcf  9144  addclprlem2  9384  mulclprlem  9386  ltexprlem7  9409  prlem936  9414  reclem4pr  9417  sqgt0sr  9472  ltord2  10078  leord2  10079  eqord2  10080  mulgt1  10397  mulge0b  10408  lt2halves  10769  addltmul  10770  zextlt  10933  recnz  10934  zeo  10944  peano5uzi  10947  uzindOLD  10953  uzm1  11112  irradd  11207  irrmul  11208  xltneg  11419  xleadd1  11450  xmulasslem  11480  xlemul1a  11483  xlemul1  11485  fznuz  11764  uznfz  11765  axdc4uzlem  12077  facndiv  12351  hashvnfin  12416  hashgt12el  12468  hashgt12el2  12469  hashf1  12493  swrdccatin2  12706  swrdccatin2d  12719  swrdccatin12d  12720  rennim  13157  cau3lem  13272  caubnd2  13275  o1lo1  13445  climrlim2  13455  climshft  13484  subcn2  13502  mulcn2  13503  rlimo1  13524  o1dif  13537  isercoll  13575  caucvgrlem  13580  serf0  13588  cvgrat  13777  efieq1re  14019  moddvds  14080  dvdseq  14120  smuval2  14219  nn0seqcvgd  14286  algcvgblem  14293  eucalglt  14301  coprmdvds  14330  isprm6  14337  rpexp  14348  rpmul  14351  eulerthlem2  14399  prmdiv  14402  pcprendvds2  14452  pcz  14491  pcprmpw  14493  pcadd2  14496  pcfac  14505  expnprm  14508  ramlb  14624  firest  14925  joineu  15842  meeteu  15856  latjlej1  15897  latjlej2  15898  latmlem1  15913  latmlem2  15914  lubun  15955  acsmapd  16010  imasgrp2  16387  issubg4  16422  psgnunilem4  16724  oddvdsnn0  16770  odmulgeq  16781  subgpgp  16819  odcau  16826  lsmlub  16885  frgpnabllem1  17079  pgpfac1lem2  17324  pgpfac1lem3a  17325  pgpfac1lem3  17326  irredrmul  17554  islmhm2  17882  lsmelval2  17929  lspsnat  17989  znidomb  18776  ip2eq  18864  lsmcss  18899  cnpnei  19935  cncls2  19944  cncls  19945  cnntr  19946  cnt0  20017  isnrm2  20029  comppfsc  20202  kqcldsat  20403  isr0  20407  hmeoopn  20436  hmeocld  20437  trufil  20580  opnsubg  20775  ghmcnp  20782  tgphaus  20784  qustgpopn  20787  tsmsgsum  20806  tsmsgsumOLD  20809  isngp4  21300  xrhmeo  21615  bndth  21627  cfilres  21904  caubl  21915  ivthlem2  22033  ovolicc2  22102  ismbf3d  22230  itg1ge0a  22287  mbfi1flim  22299  itg2gt0  22336  dvge0  22576  dvcnvrelem1  22587  dvcvx  22590  mdegmullem  22647  ig1peu  22741  plyco  22807  coemulc  22821  dgreq0  22831  dgrlt  22832  plymul0or  22846  plydiveu  22863  quotcan  22874  aalioulem3  22899  ulmcaulem  22958  sincosq3sgn  23062  sincosq4sgn  23063  sineq0  23083  logrec  23305  xrlimcnp  23499  cxploglim  23508  sgmss  23581  mumul  23656  chtub  23688  perfect1  23704  dchrelbas3  23714  lgsdir2lem4  23802  lgsne0  23809  lgsquad2lem2  23835  2sqlem8a  23847  2sqblem  23853  axcontlem2  24473  cusgrarn  24664  redwlk  24813  wlkdvspth  24815  wlkiswwlk1  24895  wlklniswwlkn1  24904  clwwlkext2edg  25007  wwlksubclwwlk  25009  clwlkf1clwwlklem  25054  frgrawopreg1  25255  frgrawopreg2  25256  extwwlkfablem2  25283  rngosn3  25629  blocnilem  25920  ip2eqi  25973  ubthlem2  25988  hial0  26220  hial02  26221  hial2eq  26224  h1datomi  26700  sumspansn  26768  lnopcnbd  27156  riesz4i  27183  bra11  27228  pjss2coi  27284  pjnormssi  27288  pjorthcoi  27289  pjclem4a  27318  pj3lem1  27326  pj3cor1i  27329  hst1h  27347  stm1i  27363  strlem1  27370  golem2  27392  mdbr2  27416  dmdbr5  27428  mdsl2i  27442  atexch  27501  atcvatlem  27505  chirredlem1  27510  cdjreui  27552  cdj1i  27553  cdj3lem1  27554  xraddge02  27811  submarchi  27967  isarchiofld  28045  esumcvg  28318  lgamgulmlem1  28838  erdsze2lem2  28915  ghomf1olem  29301  btwnexch  29906  btwncolinear2  29951  btwncolinear3  29952  btwncolinear4  29953  btwncolinear5  29954  btwncolinear6  29955  onsuct0  30137  onint1  30145  ltflcei  30286  tan2h  30290  ftc1anclem6  30338  dvasin  30346  dvacos  30347  nn0prpw  30384  cldbnd  30387  fdc  30481  caushft  30497  heibor1lem  30548  bfplem2  30562  rrncmslem  30571  mpt2bi123f  30814  ctbnfien  30994  rmxypairf1o  31089  monotoddzzfi  31120  oddcomabszz  31122  acongtr  31158  lcmgcdlem  31456  expgrowth  31484  funressnfv  32455  2elfz2melfz  32727  uzlidlring  33008  ply1mulgsumlem2  33260  fllog2  33462  dignn0flhalflem1  33509  sbcbi  33719  csbeq2gOLD  33735  bnj1468  34324  bj-ceqsalt0  34869  bj-ceqsalt1  34870  bj-inftyexpiinj  35031  bj-bary1lem1  35096  bj-bary1  35097  riotasv3d  35107  lsatcv1  35189  lub0N  35330  glb0N  35334  oplecon3b  35341  cmtbr4N  35396  cvrnbtwn2  35416  atnlt  35454  atlatle  35461  cvlsupr2  35484  cvrexchlem  35559  cvratlem  35561  atcvrj0  35568  cvrat4  35583  cvrat42  35584  4noncolr3  35593  ps-1  35617  llnnlt  35663  lplnnlt  35705  lvolnltN  35758  dalempnes  35791  dalemqnet  35792  dalem-cly  35811  dalem44  35856  pmaple  35901  cdlemblem  35933  paddss  35985  2polcon4bN  36058  ltrneq2  36288  cdlemc3  36334  cdleme11h  36407  cdleme16b  36420  cdlemednpq  36440  tendospcanN  37166  dihmeetlem13N  37462  mapdordlem2  37780  mapdn0  37812
  Copyright terms: Public domain W3C validator