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

Theorem sylibd 205
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 198 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 40 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  3imtr3d  258  ceqsalt  2823  sbceqal  3055  sbcimdv  3065  csbiebt  3130  rspcsbela  3153  copsexg  4268  ordzsl  4652  isoselem  5854  riotass2  6348  riotasv3d  6369  riotasv3dOLD  6370  oaword2  6567  oaordex  6572  omword1  6587  om00  6589  omeulem2  6597  oen0  6600  oeeui  6616  nnaordex  6652  php3  7063  onomeneq  7066  frfi  7118  suc11reg  7336  cardne  7614  cardsdomel  7623  carduni  7630  acndom  7694  alephinit  7738  cfflb  7901  cfslb2n  7910  fin23lem28  7982  isf34lem6  8022  fin1a2lem9  8050  axcc3  8080  winalim2  8334  inar1  8413  rankcf  8415  addclprlem2  8657  mulclprlem  8659  ltexprlem7  8682  prlem936  8687  reclem4pr  8690  sqgt0sr  8744  ltord2  9318  leord2  9319  eqord2  9320  mulgt1  9631  lt2halves  9962  addltmul  9963  zextlt  10102  recnz  10103  zeo  10113  peano5uzi  10116  uzindOLD  10122  uzm1  10274  irradd  10356  irrmul  10357  xltneg  10560  xleadd1  10591  xmulasslem  10621  xlemul1a  10624  xlemul1  10626  fznuz  10880  uznfz  10881  axdc4uzlem  11060  facndiv  11317  hashf1  11411  rennim  11740  cau3lem  11854  caubnd2  11857  o1lo1  12027  climrlim2  12037  climshft  12066  subcn2  12084  mulcn2  12085  rlimo1  12106  o1dif  12119  isercoll  12157  caucvgrlem  12161  serf0  12169  cvgrat  12355  efieq1re  12495  moddvds  12554  dvdseq  12592  smuval2  12689  nn0seqcvgd  12756  algcvgblem  12763  eucalglt  12771  coprmdvds  12797  isprm6  12804  rpexp  12815  rpmul  12818  eulerthlem2  12866  prmdiv  12869  pcprendvds2  12910  pcz  12949  pcprmpw  12951  pcadd2  12954  pcfac  12963  expnprm  12966  ramlb  13082  firest  13353  latjlej1  14187  latjlej2  14188  latmlem1  14203  latmlem2  14204  lubun  14243  acsmapd  14297  imasgrp2  14626  issubg4  14654  oddvdsnn0  14875  odmulgeq  14886  subgpgp  14924  odcau  14931  lsmlub  14990  frgpnabllem1  15177  pgpfac1lem2  15326  pgpfac1lem3a  15327  pgpfac1lem3  15328  irredrmul  15505  islmhm2  15811  lsmelval2  15854  lspsnat  15914  znidomb  16531  ip2eq  16573  lsmcss  16608  cnpnei  17009  cncls2  17018  cncls  17019  cnntr  17020  cnt0  17090  isnrm2  17102  kqcldsat  17440  isr0  17444  hmeoopn  17473  hmeocld  17474  trufil  17621  opnsubg  17806  ghmcnp  17813  tgphaus  17815  divstgpopn  17818  tsmsgsum  17837  isngp4  18149  xrhmeo  18460  bndth  18472  cfilres  18738  caubl  18749  ivthlem2  18828  ovolicc2  18897  ismbf3d  19025  itg1ge0a  19082  mbfi1flim  19094  itg2gt0  19131  dvge0  19369  dvcnvrelem1  19380  dvcvx  19383  mdegmullem  19480  ig1peu  19573  plyco  19639  coemulc  19652  dgreq0  19662  dgrlt  19663  plymul0or  19677  plydiveu  19694  quotcan  19705  aalioulem3  19730  ulmcaulem  19787  sincosq3sgn  19884  sincosq4sgn  19885  sineq0  19905  logrec  20133  xrlimcnp  20279  cxploglim  20288  sgmss  20360  mumul  20435  chtub  20467  perfect1  20483  dchrelbas3  20493  lgsdir2lem4  20581  lgsne0  20588  lgsquad2lem2  20614  2sqlem8a  20626  2sqblem  20632  rngosn3  21109  blocnilem  21398  ip2eqi  21451  ubthlem2  21466  hial0  21697  hial02  21698  hial2eq  21701  h1datomi  22176  sumspansn  22244  lnopcnbd  22632  riesz4i  22659  bra11  22704  pjss2coi  22760  pjnormssi  22764  pjorthcoi  22765  pjclem4a  22794  pj3lem1  22802  pj3cor1i  22805  hst1h  22823  stm1i  22839  strlem1  22846  golem2  22868  mdbr2  22892  dmdbr5  22904  mdsl2i  22918  atexch  22977  atcvatlem  22981  chirredlem1  22986  cdjreui  23028  cdj1i  23029  cdj3lem1  23030  xraddge02  23267  esumcvg  23469  erdsze2lem2  23750  ghomf1olem  24016  mulge0b  24101  axcontlem2  24665  btwnexch  24720  btwncolinear2  24765  btwncolinear3  24766  btwncolinear4  24767  btwncolinear5  24768  btwncolinear6  24769  onsuct0  24952  onint1  24960  ltflcei  24998  dvreasin  25026  trooo  25497  filint2  25656  idmon  25920  nn0prpw  26342  cldbnd  26347  comppfsc  26410  fdc  26558  caushft  26580  heibor1lem  26636  bfplem2  26650  rrncmslem  26659  ctbnfien  27004  rmxypairf1o  27099  monotoddzzfi  27130  oddcomabszz  27132  acongtr  27168  psgnunilem4  27523  expgrowth  27655  funressnfv  28096  hashgt12el  28218  hashgt12el2  28219  redwlk  28364  wlkdvspth  28366  sbcbi  28602  csbeq2g  28614  bnj1468  29194  lubunNEW  29785  lsatcv1  29860  lub0N  30001  glb0N  30005  oplecon3b  30012  cmtbr4N  30067  cvrnbtwn2  30087  atnlt  30125  atlatle  30132  cvlsupr2  30155  cvrexchlem  30230  cvratlem  30232  atcvrj0  30239  cvrat4  30254  cvrat42  30255  4noncolr3  30264  ps-1  30288  llnnlt  30334  lplnnlt  30376  lvolnltN  30429  dalempnes  30462  dalemqnet  30463  dalem-cly  30482  dalem44  30527  pmaple  30572  cdlemblem  30604  paddss  30656  2polcon4bN  30729  ltrneq2  30959  cdlemc3  31004  cdleme11h  31077  cdleme16b  31090  cdlemednpq  31110  tendospcanN  31835  dihmeetlem13N  32131  mapdordlem2  32449  mapdn0  32481
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 177
  Copyright terms: Public domain W3C validator