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  3136  sbceqal  3387  sbcimdvOLD  3401  csbiebt  3455  rspcsbela  3853  copsexgOLD  4733  elrnrexdm  6025  isoselem  6225  riotass2  6272  ordzsl  6664  oaword2  7202  oaordex  7207  omword1  7222  om00  7224  omeulem2  7232  oen0  7235  oeeui  7251  nnaordex  7287  php3  7703  onomeneq  7707  frfi  7765  suc11reg  8036  cardne  8346  cardsdomel  8355  carduni  8362  acndom  8432  alephinit  8476  cfflb  8639  cfslb2n  8648  fin23lem28  8720  isf34lem6  8760  fin1a2lem9  8788  axcc3  8818  winalim2  9074  inar1  9153  rankcf  9155  addclprlem2  9395  mulclprlem  9397  ltexprlem7  9420  prlem936  9425  reclem4pr  9428  sqgt0sr  9483  ltord2  10082  leord2  10083  eqord2  10084  mulgt1  10401  mulge0b  10412  lt2halves  10773  addltmul  10774  zextlt  10935  recnz  10936  zeo  10946  peano5uzi  10949  uzindOLD  10955  uzm1  11112  irradd  11206  irrmul  11207  xltneg  11416  xleadd1  11447  xmulasslem  11477  xlemul1a  11480  xlemul1  11482  fznuz  11760  uznfz  11761  axdc4uzlem  12060  facndiv  12334  hashvnfin  12399  hashgt12el  12446  hashgt12el2  12447  hashf1  12472  swrdccatin2  12675  swrdccatin2d  12688  swrdccatin12d  12689  rennim  13035  cau3lem  13150  caubnd2  13153  o1lo1  13323  climrlim2  13333  climshft  13362  subcn2  13380  mulcn2  13381  rlimo1  13402  o1dif  13415  isercoll  13453  caucvgrlem  13458  serf0  13466  cvgrat  13655  efieq1re  13795  moddvds  13854  dvdseq  13892  smuval2  13991  nn0seqcvgd  14058  algcvgblem  14065  eucalglt  14073  coprmdvds  14102  isprm6  14109  rpexp  14120  rpmul  14123  eulerthlem2  14171  prmdiv  14174  pcprendvds2  14224  pcz  14263  pcprmpw  14265  pcadd2  14268  pcfac  14277  expnprm  14280  ramlb  14396  firest  14688  joineu  15497  meeteu  15511  latjlej1  15552  latjlej2  15553  latmlem1  15568  latmlem2  15569  lubun  15610  acsmapd  15665  imasgrp2  15995  issubg4  16025  psgnunilem4  16328  oddvdsnn0  16374  odmulgeq  16385  subgpgp  16423  odcau  16430  lsmlub  16489  frgpnabllem1  16680  pgpfac1lem2  16928  pgpfac1lem3a  16929  pgpfac1lem3  16930  irredrmul  17157  islmhm2  17484  lsmelval2  17531  lspsnat  17591  znidomb  18395  ip2eq  18483  lsmcss  18518  cnpnei  19559  cncls2  19568  cncls  19569  cnntr  19570  cnt0  19641  isnrm2  19653  kqcldsat  19997  isr0  20001  hmeoopn  20030  hmeocld  20031  trufil  20174  opnsubg  20369  ghmcnp  20376  tgphaus  20378  divstgpopn  20381  tsmsgsum  20400  tsmsgsumOLD  20403  isngp4  20894  xrhmeo  21209  bndth  21221  cfilres  21498  caubl  21509  ivthlem2  21627  ovolicc2  21696  ismbf3d  21824  itg1ge0a  21881  mbfi1flim  21893  itg2gt0  21930  dvge0  22170  dvcnvrelem1  22181  dvcvx  22184  mdegmullem  22241  ig1peu  22335  plyco  22401  coemulc  22414  dgreq0  22424  dgrlt  22425  plymul0or  22439  plydiveu  22456  quotcan  22467  aalioulem3  22492  ulmcaulem  22551  sincosq3sgn  22654  sincosq4sgn  22655  sineq0  22675  logrec  22907  xrlimcnp  23054  cxploglim  23063  sgmss  23136  mumul  23211  chtub  23243  perfect1  23259  dchrelbas3  23269  lgsdir2lem4  23357  lgsne0  23364  lgsquad2lem2  23390  2sqlem8a  23402  2sqblem  23408  axcontlem2  23972  cusgrarn  24163  redwlk  24312  wlkdvspth  24314  wlkiswwlk1  24394  wlklniswwlkn1  24403  clwwlkext2edg  24506  wwlksubclwwlk  24508  clwlkf1clwwlklem  24553  frgrawopreg1  24755  frgrawopreg2  24756  extwwlkfablem2  24783  rngosn3  25132  blocnilem  25423  ip2eqi  25476  ubthlem2  25491  hial0  25723  hial02  25724  hial2eq  25727  h1datomi  26203  sumspansn  26271  lnopcnbd  26659  riesz4i  26686  bra11  26731  pjss2coi  26787  pjnormssi  26791  pjorthcoi  26792  pjclem4a  26821  pj3lem1  26829  pj3cor1i  26832  hst1h  26850  stm1i  26866  strlem1  26873  golem2  26895  mdbr2  26919  dmdbr5  26931  mdsl2i  26945  atexch  27004  atcvatlem  27008  chirredlem1  27013  cdjreui  27055  cdj1i  27056  cdj3lem1  27057  xraddge02  27273  submarchi  27420  isarchiofld  27498  esumcvg  27760  lgamgulmlem1  28239  erdsze2lem2  28316  ghomf1olem  28537  btwnexch  29280  btwncolinear2  29325  btwncolinear3  29326  btwncolinear4  29327  btwncolinear5  29328  btwncolinear6  29329  onsuct0  29511  onint1  29519  ltflcei  29648  tan2h  29652  ftc1anclem6  29700  dvasin  29708  dvacos  29709  nn0prpw  29746  cldbnd  29749  comppfsc  29807  fdc  29869  caushft  29885  heibor1lem  29936  bfplem2  29950  rrncmslem  29959  mpt2bi123f  30203  ctbnfien  30384  rmxypairf1o  30479  monotoddzzfi  30510  oddcomabszz  30512  acongtr  30548  lcmgcdlem  30840  expgrowth  30868  funressnfv  31708  2elfz2melfz  31829  ply1mulgsumlem2  32086  sbcbi  32408  csbeq2gOLD  32420  bnj1468  33001  bj-ceqsalt0  33548  bj-ceqsalt1  33549  bj-inftyexpiinj  33702  bj-bary1lem1  33770  bj-bary1  33771  riotasv3d  33781  lsatcv1  33863  lub0N  34004  glb0N  34008  oplecon3b  34015  cmtbr4N  34070  cvrnbtwn2  34090  atnlt  34128  atlatle  34135  cvlsupr2  34158  cvrexchlem  34233  cvratlem  34235  atcvrj0  34242  cvrat4  34257  cvrat42  34258  4noncolr3  34267  ps-1  34291  llnnlt  34337  lplnnlt  34379  lvolnltN  34432  dalempnes  34465  dalemqnet  34466  dalem-cly  34485  dalem44  34530  pmaple  34575  cdlemblem  34607  paddss  34659  2polcon4bN  34732  ltrneq2  34962  cdlemc3  35007  cdleme11h  35080  cdleme16b  35093  cdlemednpq  35113  tendospcanN  35838  dihmeetlem13N  36134  mapdordlem2  36452  mapdn0  36484
  Copyright terms: Public domain W3C validator