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  2985  sbceqal  3230  sbcimdvOLD  3244  csbiebt  3296  rspcsbela  3693  copsexg  4564  copsexgOLD  4565  elrnrexdm  5835  isoselem  6019  riotass2  6067  ordzsl  6445  oaword2  6980  oaordex  6985  omword1  7000  om00  7002  omeulem2  7010  oen0  7013  oeeui  7029  nnaordex  7065  php3  7485  onomeneq  7488  frfi  7545  suc11reg  7813  cardne  8123  cardsdomel  8132  carduni  8139  acndom  8209  alephinit  8253  cfflb  8416  cfslb2n  8425  fin23lem28  8497  isf34lem6  8537  fin1a2lem9  8565  axcc3  8595  winalim2  8850  inar1  8929  rankcf  8931  addclprlem2  9173  mulclprlem  9175  ltexprlem7  9198  prlem936  9203  reclem4pr  9206  sqgt0sr  9260  ltord2  9856  leord2  9857  eqord2  9858  mulgt1  10175  mulge0b  10186  lt2halves  10546  addltmul  10547  zextlt  10703  recnz  10704  zeo  10714  peano5uzi  10717  uzindOLD  10723  uzm1  10878  irradd  10964  irrmul  10965  xltneg  11174  xleadd1  11205  xmulasslem  11235  xlemul1a  11238  xlemul1  11240  fznuz  11525  uznfz  11526  axdc4uzlem  11787  facndiv  12047  hashvnfin  12112  hashgt12el  12156  hashgt12el2  12157  hashf1  12193  swrdccatin2  12361  swrdccatin2d  12374  swrdccatin12d  12375  rennim  12711  cau3lem  12825  caubnd2  12828  o1lo1  12998  climrlim2  13008  climshft  13037  subcn2  13055  mulcn2  13056  rlimo1  13077  o1dif  13090  isercoll  13128  caucvgrlem  13133  serf0  13141  cvgrat  13325  efieq1re  13465  moddvds  13524  dvdseq  13562  smuval2  13660  nn0seqcvgd  13727  algcvgblem  13734  eucalglt  13742  coprmdvds  13770  isprm6  13777  rpexp  13788  rpmul  13791  eulerthlem2  13839  prmdiv  13842  pcprendvds2  13890  pcz  13929  pcprmpw  13931  pcadd2  13934  pcfac  13943  expnprm  13946  ramlb  14062  firest  14353  joineu  15162  meeteu  15176  latjlej1  15217  latjlej2  15218  latmlem1  15233  latmlem2  15234  lubun  15275  acsmapd  15330  imasgrp2  15649  issubg4  15679  psgnunilem4  15982  oddvdsnn0  16026  odmulgeq  16037  subgpgp  16075  odcau  16082  lsmlub  16141  frgpnabllem1  16330  pgpfac1lem2  16549  pgpfac1lem3a  16550  pgpfac1lem3  16551  irredrmul  16732  islmhm2  17040  lsmelval2  17087  lspsnat  17147  znidomb  17835  ip2eq  17923  lsmcss  17958  cnpnei  18709  cncls2  18718  cncls  18719  cnntr  18720  cnt0  18791  isnrm2  18803  kqcldsat  19147  isr0  19151  hmeoopn  19180  hmeocld  19181  trufil  19324  opnsubg  19519  ghmcnp  19526  tgphaus  19528  divstgpopn  19531  tsmsgsum  19550  tsmsgsumOLD  19553  isngp4  20044  xrhmeo  20359  bndth  20371  cfilres  20648  caubl  20659  ivthlem2  20777  ovolicc2  20846  ismbf3d  20973  itg1ge0a  21030  mbfi1flim  21042  itg2gt0  21079  dvge0  21319  dvcnvrelem1  21330  dvcvx  21333  mdegmullem  21433  ig1peu  21527  plyco  21593  coemulc  21606  dgreq0  21616  dgrlt  21617  plymul0or  21631  plydiveu  21648  quotcan  21659  aalioulem3  21684  ulmcaulem  21743  sincosq3sgn  21846  sincosq4sgn  21847  sineq0  21867  logrec  22099  xrlimcnp  22246  cxploglim  22255  sgmss  22328  mumul  22403  chtub  22435  perfect1  22451  dchrelbas3  22461  lgsdir2lem4  22549  lgsne0  22556  lgsquad2lem2  22582  2sqlem8a  22594  2sqblem  22600  axcontlem2  23033  cusgrarn  23189  redwlk  23327  wlkdvspth  23329  rngosn3  23735  blocnilem  24026  ip2eqi  24079  ubthlem2  24094  hial0  24326  hial02  24327  hial2eq  24330  h1datomi  24806  sumspansn  24874  lnopcnbd  25262  riesz4i  25289  bra11  25334  pjss2coi  25390  pjnormssi  25394  pjorthcoi  25395  pjclem4a  25424  pj3lem1  25432  pj3cor1i  25435  hst1h  25453  stm1i  25469  strlem1  25476  golem2  25498  mdbr2  25522  dmdbr5  25534  mdsl2i  25548  atexch  25607  atcvatlem  25611  chirredlem1  25616  cdjreui  25658  cdj1i  25659  cdj3lem1  25660  xraddge02  25874  submarchi  26026  isarchiofld  26137  esumcvg  26388  lgamgulmlem1  26862  erdsze2lem2  26939  ghomf1olem  27159  btwnexch  27902  btwncolinear2  27947  btwncolinear3  27948  btwncolinear4  27949  btwncolinear5  27950  btwncolinear6  27951  onsuct0  28134  onint1  28142  ltflcei  28260  tan2h  28265  ftc1anclem6  28313  dvasin  28321  dvacos  28322  nn0prpw  28359  cldbnd  28362  comppfsc  28420  fdc  28482  caushft  28498  heibor1lem  28549  bfplem2  28563  rrncmslem  28572  ctbnfien  28999  rmxypairf1o  29094  monotoddzzfi  29125  oddcomabszz  29127  acongtr  29163  expgrowth  29451  funressnfv  29877  2elfz2melfz  30045  wlkiswwlk1  30167  wlklniswwlkn1  30176  clwwlkext2edg  30307  wwlksubclwwlk  30309  clwlkf1clwwlklem  30365  frgrawopreg1  30486  frgrawopreg2  30487  extwwlkfablem2  30514  sbcbi  30944  csbeq2gOLD  30956  bnj1468  31538  bj-ceqsalt  31985  bj-inftyexpiinj  32109  bj-bary1lem1  32172  bj-bary1  32173  riotasv3d  32181  lsatcv1  32263  lub0N  32404  glb0N  32408  oplecon3b  32415  cmtbr4N  32470  cvrnbtwn2  32490  atnlt  32528  atlatle  32535  cvlsupr2  32558  cvrexchlem  32633  cvratlem  32635  atcvrj0  32642  cvrat4  32657  cvrat42  32658  4noncolr3  32667  ps-1  32691  llnnlt  32737  lplnnlt  32779  lvolnltN  32832  dalempnes  32865  dalemqnet  32866  dalem-cly  32885  dalem44  32930  pmaple  32975  cdlemblem  33007  paddss  33059  2polcon4bN  33132  ltrneq2  33362  cdlemc3  33407  cdleme11h  33480  cdleme16b  33493  cdlemednpq  33513  tendospcanN  34238  dihmeetlem13N  34534  mapdordlem2  34852  mapdn0  34884
  Copyright terms: Public domain W3C validator