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  2810  sbceqal  3042  sbcimdv  3052  csbiebt  3117  rspcsbela  3140  copsexg  4252  ordzsl  4636  isoselem  5838  riotass2  6332  riotasv3d  6353  riotasv3dOLD  6354  oaword2  6551  oaordex  6556  omword1  6571  om00  6573  omeulem2  6581  oen0  6584  oeeui  6600  nnaordex  6636  php3  7047  onomeneq  7050  frfi  7102  suc11reg  7320  cardne  7598  cardsdomel  7607  carduni  7614  acndom  7678  alephinit  7722  cfflb  7885  cfslb2n  7894  fin23lem28  7966  isf34lem6  8006  fin1a2lem9  8034  axcc3  8064  winalim2  8318  inar1  8397  rankcf  8399  addclprlem2  8641  mulclprlem  8643  ltexprlem7  8666  prlem936  8671  reclem4pr  8674  sqgt0sr  8728  ltord2  9302  leord2  9303  eqord2  9304  mulgt1  9615  lt2halves  9946  addltmul  9947  zextlt  10086  recnz  10087  zeo  10097  peano5uzi  10100  uzindOLD  10106  uzm1  10258  irradd  10340  irrmul  10341  xltneg  10544  xleadd1  10575  xmulasslem  10605  xlemul1a  10608  xlemul1  10610  fznuz  10864  uznfz  10865  axdc4uzlem  11044  facndiv  11301  hashf1  11395  rennim  11724  cau3lem  11838  caubnd2  11841  o1lo1  12011  climrlim2  12021  climshft  12050  subcn2  12068  mulcn2  12069  rlimo1  12090  o1dif  12103  isercoll  12141  caucvgrlem  12145  serf0  12153  cvgrat  12339  efieq1re  12479  moddvds  12538  dvdseq  12576  smuval2  12673  nn0seqcvgd  12740  algcvgblem  12747  eucalglt  12755  coprmdvds  12781  isprm6  12788  rpexp  12799  rpmul  12802  eulerthlem2  12850  prmdiv  12853  pcprendvds2  12894  pcz  12933  pcprmpw  12935  pcadd2  12938  pcfac  12947  expnprm  12950  ramlb  13066  firest  13337  latjlej1  14171  latjlej2  14172  latmlem1  14187  latmlem2  14188  lubun  14227  acsmapd  14281  imasgrp2  14610  issubg4  14638  oddvdsnn0  14859  odmulgeq  14870  subgpgp  14908  odcau  14915  lsmlub  14974  frgpnabllem1  15161  pgpfac1lem2  15310  pgpfac1lem3a  15311  pgpfac1lem3  15312  irredrmul  15489  islmhm2  15795  lsmelval2  15838  lspsnat  15898  znidomb  16515  ip2eq  16557  lsmcss  16592  cnpnei  16993  cncls2  17002  cncls  17003  cnntr  17004  cnt0  17074  isnrm2  17086  kqcldsat  17424  isr0  17428  hmeoopn  17457  hmeocld  17458  trufil  17605  opnsubg  17790  ghmcnp  17797  tgphaus  17799  divstgpopn  17802  tsmsgsum  17821  isngp4  18133  xrhmeo  18444  bndth  18456  cfilres  18722  caubl  18733  ivthlem2  18812  ovolicc2  18881  ismbf3d  19009  itg1ge0a  19066  mbfi1flim  19078  itg2gt0  19115  dvge0  19353  dvcnvrelem1  19364  dvcvx  19367  mdegmullem  19464  ig1peu  19557  plyco  19623  coemulc  19636  dgreq0  19646  dgrlt  19647  plymul0or  19661  plydiveu  19678  quotcan  19689  aalioulem3  19714  ulmcaulem  19771  sincosq3sgn  19868  sincosq4sgn  19869  sineq0  19889  logrec  20117  xrlimcnp  20263  cxploglim  20272  sgmss  20344  mumul  20419  chtub  20451  perfect1  20467  dchrelbas3  20477  lgsdir2lem4  20565  lgsne0  20572  lgsquad2lem2  20598  2sqlem8a  20610  2sqblem  20616  rngosn3  21093  blocnilem  21382  ip2eqi  21435  ubthlem2  21450  hial0  21681  hial02  21682  hial2eq  21685  h1datomi  22160  sumspansn  22228  lnopcnbd  22616  riesz4i  22643  bra11  22688  pjss2coi  22744  pjnormssi  22748  pjorthcoi  22749  pjclem4a  22778  pj3lem1  22786  pj3cor1i  22789  hst1h  22807  stm1i  22823  strlem1  22830  golem2  22852  mdbr2  22876  dmdbr5  22888  mdsl2i  22902  atexch  22961  atcvatlem  22965  chirredlem1  22970  cdjreui  23012  cdj1i  23013  cdj3lem1  23014  xraddge02  23252  esumcvg  23454  erdsze2lem2  23735  ghomf1olem  24001  mulge0b  24086  axcontlem2  24593  btwnexch  24648  btwncolinear2  24693  btwncolinear3  24694  btwncolinear4  24695  btwncolinear5  24696  btwncolinear6  24697  onsuct0  24880  onint1  24888  dvreasin  24923  trooo  25394  filint2  25553  idmon  25817  nn0prpw  26239  cldbnd  26244  comppfsc  26307  fdc  26455  caushft  26477  heibor1lem  26533  bfplem2  26547  rrncmslem  26556  ctbnfien  26901  rmxypairf1o  26996  monotoddzzfi  27027  oddcomabszz  27029  acongtr  27065  psgnunilem4  27420  expgrowth  27552  funressnfv  27991  sbcbi  28303  csbeq2g  28315  bnj1468  28878  lubunNEW  29163  lsatcv1  29238  lub0N  29379  glb0N  29383  oplecon3b  29390  cmtbr4N  29445  cvrnbtwn2  29465  atnlt  29503  atlatle  29510  cvlsupr2  29533  cvrexchlem  29608  cvratlem  29610  atcvrj0  29617  cvrat4  29632  cvrat42  29633  4noncolr3  29642  ps-1  29666  llnnlt  29712  lplnnlt  29754  lvolnltN  29807  dalempnes  29840  dalemqnet  29841  dalem-cly  29860  dalem44  29905  pmaple  29950  cdlemblem  29982  paddss  30034  2polcon4bN  30107  ltrneq2  30337  cdlemc3  30382  cdleme11h  30455  cdleme16b  30468  cdlemednpq  30488  tendospcanN  31213  dihmeetlem13N  31509  mapdordlem2  31827  mapdn0  31859
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