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  3118  sbceqal  3369  sbcimdvOLD  3383  csbiebt  3440  rspcsbela  3839  copsexgOLD  4723  elrnrexdm  6020  isoselem  6222  riotass2  6269  ordzsl  6665  oaword2  7204  oaordex  7209  omword1  7224  om00  7226  omeulem2  7234  oen0  7237  oeeui  7253  nnaordex  7289  php3  7705  onomeneq  7709  frfi  7767  suc11reg  8039  cardne  8349  cardsdomel  8358  carduni  8365  acndom  8435  alephinit  8479  cfflb  8642  cfslb2n  8651  fin23lem28  8723  isf34lem6  8763  fin1a2lem9  8791  axcc3  8821  winalim2  9077  inar1  9156  rankcf  9158  addclprlem2  9398  mulclprlem  9400  ltexprlem7  9423  prlem936  9428  reclem4pr  9431  sqgt0sr  9486  ltord2  10089  leord2  10090  eqord2  10091  mulgt1  10408  mulge0b  10419  lt2halves  10780  addltmul  10781  zextlt  10944  recnz  10945  zeo  10955  peano5uzi  10958  uzindOLD  10964  uzm1  11121  irradd  11216  irrmul  11217  xltneg  11426  xleadd1  11457  xmulasslem  11487  xlemul1a  11490  xlemul1  11492  fznuz  11770  uznfz  11771  axdc4uzlem  12073  facndiv  12347  hashvnfin  12412  hashgt12el  12462  hashgt12el2  12463  hashf1  12487  swrdccatin2  12693  swrdccatin2d  12706  swrdccatin12d  12707  rennim  13053  cau3lem  13168  caubnd2  13171  o1lo1  13341  climrlim2  13351  climshft  13380  subcn2  13398  mulcn2  13399  rlimo1  13420  o1dif  13433  isercoll  13471  caucvgrlem  13476  serf0  13484  cvgrat  13673  efieq1re  13915  moddvds  13974  dvdseq  14014  smuval2  14113  nn0seqcvgd  14180  algcvgblem  14187  eucalglt  14195  coprmdvds  14224  isprm6  14231  rpexp  14242  rpmul  14245  eulerthlem2  14293  prmdiv  14296  pcprendvds2  14346  pcz  14385  pcprmpw  14387  pcadd2  14390  pcfac  14399  expnprm  14402  ramlb  14518  firest  14811  joineu  15618  meeteu  15632  latjlej1  15673  latjlej2  15674  latmlem1  15689  latmlem2  15690  lubun  15731  acsmapd  15786  imasgrp2  16163  issubg4  16198  psgnunilem4  16500  oddvdsnn0  16546  odmulgeq  16557  subgpgp  16595  odcau  16602  lsmlub  16661  frgpnabllem1  16855  pgpfac1lem2  17104  pgpfac1lem3a  17105  pgpfac1lem3  17106  irredrmul  17334  islmhm2  17662  lsmelval2  17709  lspsnat  17769  znidomb  18577  ip2eq  18665  lsmcss  18700  cnpnei  19742  cncls2  19751  cncls  19752  cnntr  19753  cnt0  19824  isnrm2  19836  comppfsc  20010  kqcldsat  20211  isr0  20215  hmeoopn  20244  hmeocld  20245  trufil  20388  opnsubg  20583  ghmcnp  20590  tgphaus  20592  qustgpopn  20595  tsmsgsum  20614  tsmsgsumOLD  20617  isngp4  21108  xrhmeo  21423  bndth  21435  cfilres  21712  caubl  21723  ivthlem2  21841  ovolicc2  21910  ismbf3d  22038  itg1ge0a  22095  mbfi1flim  22107  itg2gt0  22144  dvge0  22384  dvcnvrelem1  22395  dvcvx  22398  mdegmullem  22455  ig1peu  22549  plyco  22615  coemulc  22628  dgreq0  22638  dgrlt  22639  plymul0or  22653  plydiveu  22670  quotcan  22681  aalioulem3  22706  ulmcaulem  22765  sincosq3sgn  22869  sincosq4sgn  22870  sineq0  22890  logrec  23127  xrlimcnp  23274  cxploglim  23283  sgmss  23356  mumul  23431  chtub  23463  perfect1  23479  dchrelbas3  23489  lgsdir2lem4  23577  lgsne0  23584  lgsquad2lem2  23610  2sqlem8a  23622  2sqblem  23628  axcontlem2  24244  cusgrarn  24435  redwlk  24584  wlkdvspth  24586  wlkiswwlk1  24666  wlklniswwlkn1  24675  clwwlkext2edg  24778  wwlksubclwwlk  24780  clwlkf1clwwlklem  24825  frgrawopreg1  25026  frgrawopreg2  25027  extwwlkfablem2  25054  rngosn3  25404  blocnilem  25695  ip2eqi  25748  ubthlem2  25763  hial0  25995  hial02  25996  hial2eq  25999  h1datomi  26475  sumspansn  26543  lnopcnbd  26931  riesz4i  26958  bra11  27003  pjss2coi  27059  pjnormssi  27063  pjorthcoi  27064  pjclem4a  27093  pj3lem1  27101  pj3cor1i  27104  hst1h  27122  stm1i  27138  strlem1  27145  golem2  27167  mdbr2  27191  dmdbr5  27203  mdsl2i  27217  atexch  27276  atcvatlem  27280  chirredlem1  27285  cdjreui  27327  cdj1i  27328  cdj3lem1  27329  xraddge02  27553  submarchi  27707  isarchiofld  27784  esumcvg  28069  lgamgulmlem1  28548  erdsze2lem2  28625  ghomf1olem  29011  btwnexch  29650  btwncolinear2  29695  btwncolinear3  29696  btwncolinear4  29697  btwncolinear5  29698  btwncolinear6  29699  onsuct0  29881  onint1  29889  ltflcei  30018  tan2h  30022  ftc1anclem6  30070  dvasin  30078  dvacos  30079  nn0prpw  30116  cldbnd  30119  fdc  30213  caushft  30229  heibor1lem  30280  bfplem2  30294  rrncmslem  30303  mpt2bi123f  30546  ctbnfien  30727  rmxypairf1o  30822  monotoddzzfi  30853  oddcomabszz  30855  acongtr  30891  lcmgcdlem  31188  expgrowth  31216  funressnfv  32051  2elfz2melfz  32172  uzlidlring  32445  ply1mulgsumlem2  32722  sbcbi  33043  csbeq2gOLD  33055  bnj1468  33637  bj-ceqsalt0  34197  bj-ceqsalt1  34198  bj-inftyexpiinj  34352  bj-bary1lem1  34420  bj-bary1  34421  riotasv3d  34431  lsatcv1  34513  lub0N  34654  glb0N  34658  oplecon3b  34665  cmtbr4N  34720  cvrnbtwn2  34740  atnlt  34778  atlatle  34785  cvlsupr2  34808  cvrexchlem  34883  cvratlem  34885  atcvrj0  34892  cvrat4  34907  cvrat42  34908  4noncolr3  34917  ps-1  34941  llnnlt  34987  lplnnlt  35029  lvolnltN  35082  dalempnes  35115  dalemqnet  35116  dalem-cly  35135  dalem44  35180  pmaple  35225  cdlemblem  35257  paddss  35309  2polcon4bN  35382  ltrneq2  35612  cdlemc3  35658  cdleme11h  35731  cdleme16b  35744  cdlemednpq  35764  tendospcanN  36490  dihmeetlem13N  36786  mapdordlem2  37104  mapdn0  37136
  Copyright terms: Public domain W3C validator