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  3016  sbceqal  3263  sbcimdvOLD  3277  csbiebt  3329  rspcsbela  3726  copsexgOLD  4598  elrnrexdm  5868  isoselem  6053  riotass2  6100  ordzsl  6477  oaword2  7013  oaordex  7018  omword1  7033  om00  7035  omeulem2  7043  oen0  7046  oeeui  7062  nnaordex  7098  php3  7518  onomeneq  7521  frfi  7578  suc11reg  7846  cardne  8156  cardsdomel  8165  carduni  8172  acndom  8242  alephinit  8286  cfflb  8449  cfslb2n  8458  fin23lem28  8530  isf34lem6  8570  fin1a2lem9  8598  axcc3  8628  winalim2  8884  inar1  8963  rankcf  8965  addclprlem2  9207  mulclprlem  9209  ltexprlem7  9232  prlem936  9237  reclem4pr  9240  sqgt0sr  9294  ltord2  9890  leord2  9891  eqord2  9892  mulgt1  10209  mulge0b  10220  lt2halves  10580  addltmul  10581  zextlt  10737  recnz  10738  zeo  10748  peano5uzi  10751  uzindOLD  10757  uzm1  10912  irradd  10998  irrmul  10999  xltneg  11208  xleadd1  11239  xmulasslem  11269  xlemul1a  11272  xlemul1  11274  fznuz  11563  uznfz  11564  axdc4uzlem  11825  facndiv  12085  hashvnfin  12150  hashgt12el  12194  hashgt12el2  12195  hashf1  12231  swrdccatin2  12399  swrdccatin2d  12412  swrdccatin12d  12413  rennim  12749  cau3lem  12863  caubnd2  12866  o1lo1  13036  climrlim2  13046  climshft  13075  subcn2  13093  mulcn2  13094  rlimo1  13115  o1dif  13128  isercoll  13166  caucvgrlem  13171  serf0  13179  cvgrat  13364  efieq1re  13504  moddvds  13563  dvdseq  13601  smuval2  13699  nn0seqcvgd  13766  algcvgblem  13773  eucalglt  13781  coprmdvds  13809  isprm6  13816  rpexp  13827  rpmul  13830  eulerthlem2  13878  prmdiv  13881  pcprendvds2  13929  pcz  13968  pcprmpw  13970  pcadd2  13973  pcfac  13982  expnprm  13985  ramlb  14101  firest  14392  joineu  15201  meeteu  15215  latjlej1  15256  latjlej2  15257  latmlem1  15272  latmlem2  15273  lubun  15314  acsmapd  15369  imasgrp2  15691  issubg4  15721  psgnunilem4  16024  oddvdsnn0  16068  odmulgeq  16079  subgpgp  16117  odcau  16124  lsmlub  16183  frgpnabllem1  16372  pgpfac1lem2  16598  pgpfac1lem3a  16599  pgpfac1lem3  16600  irredrmul  16821  islmhm2  17141  lsmelval2  17188  lspsnat  17248  znidomb  18016  ip2eq  18104  lsmcss  18139  cnpnei  18890  cncls2  18899  cncls  18900  cnntr  18901  cnt0  18972  isnrm2  18984  kqcldsat  19328  isr0  19332  hmeoopn  19361  hmeocld  19362  trufil  19505  opnsubg  19700  ghmcnp  19707  tgphaus  19709  divstgpopn  19712  tsmsgsum  19731  tsmsgsumOLD  19734  isngp4  20225  xrhmeo  20540  bndth  20552  cfilres  20829  caubl  20840  ivthlem2  20958  ovolicc2  21027  ismbf3d  21154  itg1ge0a  21211  mbfi1flim  21223  itg2gt0  21260  dvge0  21500  dvcnvrelem1  21511  dvcvx  21514  mdegmullem  21571  ig1peu  21665  plyco  21731  coemulc  21744  dgreq0  21754  dgrlt  21755  plymul0or  21769  plydiveu  21786  quotcan  21797  aalioulem3  21822  ulmcaulem  21881  sincosq3sgn  21984  sincosq4sgn  21985  sineq0  22005  logrec  22237  xrlimcnp  22384  cxploglim  22393  sgmss  22466  mumul  22541  chtub  22573  perfect1  22589  dchrelbas3  22599  lgsdir2lem4  22687  lgsne0  22694  lgsquad2lem2  22720  2sqlem8a  22732  2sqblem  22738  axcontlem2  23233  cusgrarn  23389  redwlk  23527  wlkdvspth  23529  rngosn3  23935  blocnilem  24226  ip2eqi  24279  ubthlem2  24294  hial0  24526  hial02  24527  hial2eq  24530  h1datomi  25006  sumspansn  25074  lnopcnbd  25462  riesz4i  25489  bra11  25534  pjss2coi  25590  pjnormssi  25594  pjorthcoi  25595  pjclem4a  25624  pj3lem1  25632  pj3cor1i  25635  hst1h  25653  stm1i  25669  strlem1  25676  golem2  25698  mdbr2  25722  dmdbr5  25734  mdsl2i  25748  atexch  25807  atcvatlem  25811  chirredlem1  25816  cdjreui  25858  cdj1i  25859  cdj3lem1  25860  xraddge02  26072  submarchi  26225  isarchiofld  26307  esumcvg  26557  lgamgulmlem1  27037  erdsze2lem2  27114  ghomf1olem  27335  btwnexch  28078  btwncolinear2  28123  btwncolinear3  28124  btwncolinear4  28125  btwncolinear5  28126  btwncolinear6  28127  onsuct0  28309  onint1  28317  ltflcei  28445  tan2h  28450  ftc1anclem6  28498  dvasin  28506  dvacos  28507  nn0prpw  28544  cldbnd  28547  comppfsc  28605  fdc  28667  caushft  28683  heibor1lem  28734  bfplem2  28748  rrncmslem  28757  mpt2bi123f  29001  ctbnfien  29183  rmxypairf1o  29278  monotoddzzfi  29309  oddcomabszz  29311  acongtr  29347  expgrowth  29635  funressnfv  30060  2elfz2melfz  30228  wlkiswwlk1  30350  wlklniswwlkn1  30359  clwwlkext2edg  30490  wwlksubclwwlk  30492  clwlkf1clwwlklem  30548  frgrawopreg1  30669  frgrawopreg2  30670  extwwlkfablem2  30697  ply1mulgsumlem2  30878  sbcbi  31342  csbeq2gOLD  31354  bnj1468  31935  bj-ceqsalt0  32480  bj-ceqsalt1  32481  bj-inftyexpiinj  32628  bj-bary1lem1  32696  bj-bary1  32697  riotasv3d  32707  lsatcv1  32789  lub0N  32930  glb0N  32934  oplecon3b  32941  cmtbr4N  32996  cvrnbtwn2  33016  atnlt  33054  atlatle  33061  cvlsupr2  33084  cvrexchlem  33159  cvratlem  33161  atcvrj0  33168  cvrat4  33183  cvrat42  33184  4noncolr3  33193  ps-1  33217  llnnlt  33263  lplnnlt  33305  lvolnltN  33358  dalempnes  33391  dalemqnet  33392  dalem-cly  33411  dalem44  33456  pmaple  33501  cdlemblem  33533  paddss  33585  2polcon4bN  33658  ltrneq2  33888  cdlemc3  33933  cdleme11h  34006  cdleme16b  34019  cdlemednpq  34039  tendospcanN  34764  dihmeetlem13N  35060  mapdordlem2  35378  mapdn0  35410
  Copyright terms: Public domain W3C validator