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

Theorem sylibd 218
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 211 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 45 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  3imtr3d  271  ceqsalt  3070  sbceqal  3319  csbiebt  3383  rspcsbela  3795  elrnrexdm  6026  isoselem  6232  riotass2  6278  ordzsl  6672  oaword2  7254  oaordex  7259  omword1  7274  om00  7276  omeulem2  7284  oen0  7287  oeeui  7303  nnaordex  7339  php3  7758  onomeneq  7762  frfi  7816  infglb  8006  suc11reg  8124  cardne  8399  cardsdomel  8408  carduni  8415  acndom  8482  alephinit  8526  cfflb  8689  cfslb2n  8698  fin23lem28  8770  isf34lem6  8810  fin1a2lem9  8838  axcc3  8868  winalim2  9121  inar1  9200  rankcf  9202  addclprlem2  9442  mulclprlem  9444  ltexprlem7  9467  prlem936  9472  reclem4pr  9475  sqgt0sr  9530  ltord2  10143  leord2  10144  eqord2  10145  mulgt1  10464  mulge0b  10475  fiminre  10555  lt2halves  10847  addltmul  10848  zextlt  11010  recnz  11011  zeo  11021  peano5uzi  11024  uzm1  11189  irradd  11288  irrmul  11289  xltneg  11510  xleadd1  11541  xmulasslem  11571  xlemul1a  11574  xlemul1  11576  fznuz  11876  uznfz  11877  axdc4uzlem  12195  facndiv  12473  hashvnfin  12541  hashgt12el  12595  hashgt12el2  12596  hashf1  12620  swrdccatin2  12843  swrdccatin2d  12856  swrdccatin12d  12857  rennim  13302  cau3lem  13417  caubnd2  13420  o1lo1  13601  climrlim2  13611  climshft  13640  subcn2  13658  mulcn2  13659  rlimo1  13680  o1dif  13693  isercoll  13731  caucvgrlem  13736  caucvgrlemOLD  13737  serf0  13747  cvgrat  13939  efieq1re  14253  moddvds  14312  dvdseq  14352  smuval2  14456  nn0seqcvgd  14529  algcvgblem  14536  eucalglt  14544  lcmgcdlem  14571  coprmdvds  14659  isprm6  14666  rpexp  14672  rpmul  14675  eulerthlem2  14730  prmdiv  14733  pcprendvds2  14791  pcz  14830  pcprmpw  14832  pcadd2  14835  pcfac  14844  expnprm  14847  ramlb  14977  prmgaplcmlem1OLD  15012  firest  15331  joineu  16256  meeteu  16270  latjlej1  16311  latjlej2  16312  latmlem1  16327  latmlem2  16328  lubun  16369  acsmapd  16424  imasgrp2  16801  issubg4  16836  psgnunilem4  17138  oddvdsnn0  17193  odmulgeq  17208  subgpgp  17249  odcau  17256  lsmlub  17315  frgpnabllem1  17509  pgpfac1lem2  17708  pgpfac1lem3a  17709  pgpfac1lem3  17710  irredrmul  17935  islmhm2  18261  lsmelval2  18308  lspsnat  18368  znidomb  19132  ip2eq  19220  lsmcss  19255  cnpnei  20280  cncls2  20289  cncls  20290  cnntr  20291  cnt0  20362  isnrm2  20374  comppfsc  20547  kqcldsat  20748  isr0  20752  hmeoopn  20781  hmeocld  20782  trufil  20925  opnsubg  21122  ghmcnp  21129  tgphaus  21131  qustgpopn  21134  tsmsgsum  21153  isngp4  21625  xrhmeo  21974  bndth  21986  cfilres  22266  caubl  22277  ivthlem2  22403  ovolicc2  22476  ismbf3d  22610  itg1ge0a  22669  mbfi1flim  22681  itg2gt0  22718  dvge0  22958  dvcnvrelem1  22969  dvcvx  22972  mdegmullem  23027  ig1peu  23122  ig1peuOLD  23123  plyco  23195  coemulc  23209  dgreq0  23219  dgrlt  23220  plymul0or  23234  plydiveu  23251  quotcan  23262  aalioulem3  23290  ulmcaulem  23349  sincosq3sgn  23455  sincosq4sgn  23456  sineq0  23476  logrec  23700  xrlimcnp  23894  cxploglim  23903  lgamgulmlem1  23954  sgmss  24033  mumul  24108  chtub  24140  perfect1  24156  dchrelbas3  24166  lgsdir2lem4  24254  lgsne0  24261  lgsquad2lem2  24287  2sqlem8a  24299  2sqblem  24305  axcontlem2  24995  cusgrarn  25187  redwlk  25336  wlkdvspth  25338  wlkiswwlk1  25418  wlklniswwlkn1  25427  clwwlkext2edg  25530  wwlksubclwwlk  25532  clwlkf1clwwlklem  25577  frgrawopreg1  25778  frgrawopreg2  25779  extwwlkfablem2  25806  rngosn3  26154  blocnilem  26445  ip2eqi  26498  ubthlem2  26513  hial0  26755  hial02  26756  hial2eq  26759  h1datomi  27234  sumspansn  27302  lnopcnbd  27689  riesz4i  27716  bra11  27761  pjss2coi  27817  pjnormssi  27821  pjorthcoi  27822  pjclem4a  27851  pj3lem1  27859  pj3cor1i  27862  hst1h  27880  stm1i  27896  strlem1  27903  golem2  27925  mdbr2  27949  dmdbr5  27961  mdsl2i  27975  atexch  28034  atcvatlem  28038  chirredlem1  28043  cdjreui  28085  cdj1i  28086  cdj3lem1  28087  xraddge02  28336  submarchi  28503  isarchiofld  28580  esumcvg  28907  bnj1468  29657  erdsze2lem2  29927  ghomf1olem  30312  btwnexch  30792  btwncolinear2  30837  btwncolinear3  30838  btwncolinear4  30839  btwncolinear5  30840  btwncolinear6  30841  nn0prpw  30979  cldbnd  30982  onsuct0  31101  onint1  31109  bj-ceqsalt0  31482  bj-ceqsalt1  31483  bj-inftyexpiinj  31651  bj-bary1lem1  31716  bj-bary1  31717  relowlssretop  31766  ltflcei  31933  tan2h  31937  poimirlem26  31966  poimirlem31  31971  ftc1anclem6  32022  dvasin  32028  dvacos  32029  fdc  32074  caushft  32090  heibor1lem  32141  bfplem2  32155  rrncmslem  32164  mpt2bi123f  32406  riotasv3d  32532  lsatcv1  32614  lub0N  32755  glb0N  32759  oplecon3b  32766  cmtbr4N  32821  cvrnbtwn2  32841  atnlt  32879  atlatle  32886  cvlsupr2  32909  cvrexchlem  32984  cvratlem  32986  atcvrj0  32993  cvrat4  33008  cvrat42  33009  4noncolr3  33018  ps-1  33042  llnnlt  33088  lplnnlt  33130  lvolnltN  33183  dalempnes  33216  dalemqnet  33217  dalem-cly  33236  dalem44  33281  pmaple  33326  cdlemblem  33358  paddss  33410  2polcon4bN  33483  ltrneq2  33713  cdlemc3  33759  cdleme11h  33832  cdleme16b  33845  cdlemednpq  33865  tendospcanN  34591  dihmeetlem13N  34887  mapdordlem2  35205  mapdn0  35237  ctbnfien  35661  rmxypairf1o  35759  monotoddzzfi  35790  oddcomabszz  35792  acongtr  35828  frege124d  36353  expgrowth  36684  sbcbi  36900  csbeq2gOLD  36916  funressnfv  38629  iccpartnel  38752  2elfz2melfz  39058  uzlidlring  39982  ply1mulgsumlem2  40232  fllog2  40432  dignn0flhalflem1  40479
  Copyright terms: Public domain W3C validator