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

Theorem sylibd 206
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 199 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 42 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  3imtr3d  259  ceqsalt  2938  sbceqal  3172  sbcimdv  3182  csbiebt  3247  rspcsbela  3268  copsexg  4402  ordzsl  4784  elrnrexdm  5833  isoselem  6020  riotass2  6536  riotasv3d  6557  riotasv3dOLD  6558  oaword2  6755  oaordex  6760  omword1  6775  om00  6777  omeulem2  6785  oen0  6788  oeeui  6804  nnaordex  6840  php3  7252  onomeneq  7255  frfi  7311  suc11reg  7530  cardne  7808  cardsdomel  7817  carduni  7824  acndom  7888  alephinit  7932  cfflb  8095  cfslb2n  8104  fin23lem28  8176  isf34lem6  8216  fin1a2lem9  8244  axcc3  8274  winalim2  8527  inar1  8606  rankcf  8608  addclprlem2  8850  mulclprlem  8852  ltexprlem7  8875  prlem936  8880  reclem4pr  8883  sqgt0sr  8937  ltord2  9512  leord2  9513  eqord2  9514  mulgt1  9825  lt2halves  10158  addltmul  10159  zextlt  10300  recnz  10301  zeo  10311  peano5uzi  10314  uzindOLD  10320  uzm1  10472  irradd  10554  irrmul  10555  xltneg  10759  xleadd1  10790  xmulasslem  10820  xlemul1a  10823  xlemul1  10825  fznuz  11084  uznfz  11085  axdc4uzlem  11276  facndiv  11534  hashvnfin  11597  hashgt12el  11637  hashgt12el2  11638  hashf1  11661  rennim  11999  cau3lem  12113  caubnd2  12116  o1lo1  12286  climrlim2  12296  climshft  12325  subcn2  12343  mulcn2  12344  rlimo1  12365  o1dif  12378  isercoll  12416  caucvgrlem  12421  serf0  12429  cvgrat  12615  efieq1re  12755  moddvds  12814  dvdseq  12852  smuval2  12949  nn0seqcvgd  13016  algcvgblem  13023  eucalglt  13031  coprmdvds  13057  isprm6  13064  rpexp  13075  rpmul  13078  eulerthlem2  13126  prmdiv  13129  pcprendvds2  13170  pcz  13209  pcprmpw  13211  pcadd2  13214  pcfac  13223  expnprm  13226  ramlb  13342  firest  13615  latjlej1  14449  latjlej2  14450  latmlem1  14465  latmlem2  14466  lubun  14505  acsmapd  14559  imasgrp2  14888  issubg4  14916  oddvdsnn0  15137  odmulgeq  15148  subgpgp  15186  odcau  15193  lsmlub  15252  frgpnabllem1  15439  pgpfac1lem2  15588  pgpfac1lem3a  15589  pgpfac1lem3  15590  irredrmul  15767  islmhm2  16069  lsmelval2  16112  lspsnat  16172  znidomb  16797  ip2eq  16839  lsmcss  16874  cnpnei  17282  cncls2  17291  cncls  17292  cnntr  17293  cnt0  17364  isnrm2  17376  kqcldsat  17718  isr0  17722  hmeoopn  17751  hmeocld  17752  trufil  17895  opnsubg  18090  ghmcnp  18097  tgphaus  18099  divstgpopn  18102  tsmsgsum  18121  isngp4  18611  xrhmeo  18924  bndth  18936  cfilres  19202  caubl  19213  ivthlem2  19302  ovolicc2  19371  ismbf3d  19499  itg1ge0a  19556  mbfi1flim  19568  itg2gt0  19605  dvge0  19843  dvcnvrelem1  19854  dvcvx  19857  mdegmullem  19954  ig1peu  20047  plyco  20113  coemulc  20126  dgreq0  20136  dgrlt  20137  plymul0or  20151  plydiveu  20168  quotcan  20179  aalioulem3  20204  ulmcaulem  20263  sincosq3sgn  20361  sincosq4sgn  20362  sineq0  20382  logrec  20614  xrlimcnp  20760  cxploglim  20769  sgmss  20842  mumul  20917  chtub  20949  perfect1  20965  dchrelbas3  20975  lgsdir2lem4  21063  lgsne0  21070  lgsquad2lem2  21096  2sqlem8a  21108  2sqblem  21114  cusgrarn  21421  redwlk  21559  wlkdvspth  21561  rngosn3  21967  blocnilem  22258  ip2eqi  22311  ubthlem2  22326  hial0  22557  hial02  22558  hial2eq  22561  h1datomi  23036  sumspansn  23104  lnopcnbd  23492  riesz4i  23519  bra11  23564  pjss2coi  23620  pjnormssi  23624  pjorthcoi  23625  pjclem4a  23654  pj3lem1  23662  pj3cor1i  23665  hst1h  23683  stm1i  23699  strlem1  23706  golem2  23728  mdbr2  23752  dmdbr5  23764  mdsl2i  23778  atexch  23837  atcvatlem  23841  chirredlem1  23846  cdjreui  23888  cdj1i  23889  cdj3lem1  23890  xraddge02  24076  esumcvg  24429  lgamgulmlem1  24766  erdsze2lem2  24843  ghomf1olem  25058  mulge0b  25144  axcontlem2  25808  btwnexch  25863  btwncolinear2  25908  btwncolinear3  25909  btwncolinear4  25910  btwncolinear5  25911  btwncolinear6  25912  onsuct0  26095  onint1  26103  ltflcei  26140  dvreasin  26179  nn0prpw  26216  cldbnd  26219  comppfsc  26277  fdc  26339  caushft  26357  heibor1lem  26408  bfplem2  26422  rrncmslem  26431  ctbnfien  26769  rmxypairf1o  26864  monotoddzzfi  26895  oddcomabszz  26897  acongtr  26933  psgnunilem4  27288  expgrowth  27420  funressnfv  27859  frgrawopreg1  28153  frgrawopreg2  28154  sbcbi  28335  csbeq2g  28347  bnj1468  28923  lubunNEW  29456  lsatcv1  29531  lub0N  29672  glb0N  29676  oplecon3b  29683  cmtbr4N  29738  cvrnbtwn2  29758  atnlt  29796  atlatle  29803  cvlsupr2  29826  cvrexchlem  29901  cvratlem  29903  atcvrj0  29910  cvrat4  29925  cvrat42  29926  4noncolr3  29935  ps-1  29959  llnnlt  30005  lplnnlt  30047  lvolnltN  30100  dalempnes  30133  dalemqnet  30134  dalem-cly  30153  dalem44  30198  pmaple  30243  cdlemblem  30275  paddss  30327  2polcon4bN  30400  ltrneq2  30630  cdlemc3  30675  cdleme11h  30748  cdleme16b  30761  cdlemednpq  30781  tendospcanN  31506  dihmeetlem13N  31802  mapdordlem2  32120  mapdn0  32152
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 178
  Copyright terms: Public domain W3C validator