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

Theorem sylibd 222
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 212 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 44 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  3imtr3d  275  ceqsalt  3056  sbceqal  3307  csbiebt  3369  rspcsbela  3799  elrnrexdm  6041  isoselem  6250  riotass2  6296  ordzsl  6691  oaword2  7272  oaordex  7277  omword1  7292  om00  7294  omeulem2  7302  oen0  7305  oeeui  7321  nnaordex  7357  php3  7776  onomeneq  7780  frfi  7834  infglb  8024  suc11reg  8142  cardne  8417  cardsdomel  8426  carduni  8433  acndom  8500  alephinit  8544  cfflb  8707  cfslb2n  8716  fin23lem28  8788  isf34lem6  8828  fin1a2lem9  8856  axcc3  8886  winalim2  9139  inar1  9218  rankcf  9220  addclprlem2  9460  mulclprlem  9462  ltexprlem7  9485  prlem936  9490  reclem4pr  9493  sqgt0sr  9548  ltord2  10164  leord2  10165  eqord2  10166  mulgt1  10486  mulge0b  10497  fiminre  10577  lt2halves  10870  addltmul  10871  zextlt  11033  recnz  11034  zeo  11044  peano5uzi  11047  uzm1  11213  irradd  11311  irrmul  11312  xltneg  11533  xleadd1  11566  xmulasslem  11596  xlemul1a  11599  xlemul1  11601  fznuz  11902  uznfz  11903  axdc4uzlem  12233  facndiv  12511  hashvnfin  12579  hashgt12el  12636  hashgt12el2  12637  hashf1  12661  ccatalpha  12787  swrdccatin2  12897  swrdccatin2d  12910  swrdccatin12d  12911  rennim  13379  cau3lem  13494  caubnd2  13497  o1lo1  13678  climrlim2  13688  climshft  13717  subcn2  13735  mulcn2  13736  rlimo1  13757  o1dif  13770  isercoll  13808  caucvgrlem  13813  caucvgrlemOLD  13814  serf0  13824  cvgrat  14016  efieq1re  14330  moddvds  14389  dvdseq  14429  smuval2  14535  nn0seqcvgd  14608  algcvgblem  14615  eucalglt  14623  lcmgcdlem  14650  coprmdvds  14738  isprm6  14745  rpexp  14751  rpmul  14754  eulerthlem2  14809  prmdiv  14812  pcprendvds2  14870  pcz  14909  pcprmpw  14911  pcadd2  14914  pcfac  14923  expnprm  14926  ramlb  15056  prmgaplcmlem1OLD  15091  firest  15409  joineu  16334  meeteu  16348  latjlej1  16389  latjlej2  16390  latmlem1  16405  latmlem2  16406  lubun  16447  acsmapd  16502  imasgrp2  16879  issubg4  16914  psgnunilem4  17216  oddvdsnn0  17271  odmulgeq  17286  subgpgp  17327  odcau  17334  lsmlub  17393  frgpnabllem1  17587  pgpfac1lem2  17786  pgpfac1lem3a  17787  pgpfac1lem3  17788  irredrmul  18013  islmhm2  18339  lsmelval2  18386  lspsnat  18446  znidomb  19209  ip2eq  19297  lsmcss  19332  cnpnei  20357  cncls2  20366  cncls  20367  cnntr  20368  cnt0  20439  isnrm2  20451  comppfsc  20624  kqcldsat  20825  isr0  20829  hmeoopn  20858  hmeocld  20859  trufil  21003  opnsubg  21200  ghmcnp  21207  tgphaus  21209  qustgpopn  21212  tsmsgsum  21231  isngp4  21703  xrhmeo  22052  bndth  22064  cfilres  22344  caubl  22355  ivthlem2  22481  ovolicc2  22554  ismbf3d  22689  itg1ge0a  22748  mbfi1flim  22760  itg2gt0  22797  dvge0  23037  dvcnvrelem1  23048  dvcvx  23051  mdegmullem  23106  ig1peu  23201  ig1peuOLD  23202  plyco  23274  coemulc  23288  dgreq0  23298  dgrlt  23299  plymul0or  23313  plydiveu  23330  quotcan  23341  aalioulem3  23369  ulmcaulem  23428  sincosq3sgn  23534  sincosq4sgn  23535  sineq0  23555  logrec  23779  xrlimcnp  23973  cxploglim  23982  lgamgulmlem1  24033  sgmss  24112  mumul  24187  chtub  24219  perfect1  24235  dchrelbas3  24245  lgsdir2lem4  24333  lgsne0  24340  lgsquad2lem2  24366  2sqlem8a  24378  2sqblem  24384  axcontlem2  25074  cusgrarn  25266  redwlk  25415  wlkdvspth  25417  wlkiswwlk1  25497  wlklniswwlkn1  25506  clwwlkext2edg  25609  wwlksubclwwlk  25611  clwlkf1clwwlklem  25656  frgrawopreg1  25857  frgrawopreg2  25858  extwwlkfablem2  25885  rngosn3  26235  blocnilem  26526  ip2eqi  26579  ubthlem2  26594  hial0  26836  hial02  26837  hial2eq  26840  h1datomi  27315  sumspansn  27383  lnopcnbd  27770  riesz4i  27797  bra11  27842  pjss2coi  27898  pjnormssi  27902  pjorthcoi  27903  pjclem4a  27932  pj3lem1  27940  pj3cor1i  27943  hst1h  27961  stm1i  27977  strlem1  27984  golem2  28006  mdbr2  28030  dmdbr5  28042  mdsl2i  28056  atexch  28115  atcvatlem  28119  chirredlem1  28124  cdjreui  28166  cdj1i  28167  cdj3lem1  28168  xraddge02  28411  submarchi  28577  isarchiofld  28654  esumcvg  28981  bnj1468  29729  erdsze2lem2  29999  ghomf1olem  30384  btwnexch  30863  btwncolinear2  30908  btwncolinear3  30909  btwncolinear4  30910  btwncolinear5  30911  btwncolinear6  30912  nn0prpw  31050  cldbnd  31053  onsuct0  31172  onint1  31180  bj-ceqsalt0  31550  bj-ceqsalt1  31551  bj-inftyexpiinj  31721  bj-bary1lem1  31786  bj-bary1  31787  relowlssretop  31836  ltflcei  31997  tan2h  32001  poimirlem26  32030  poimirlem31  32035  ftc1anclem6  32086  dvasin  32092  dvacos  32093  fdc  32138  caushft  32154  heibor1lem  32205  bfplem2  32219  rrncmslem  32228  mpt2bi123f  32470  riotasv3d  32596  lsatcv1  32685  lub0N  32826  glb0N  32830  oplecon3b  32837  cmtbr4N  32892  cvrnbtwn2  32912  atnlt  32950  atlatle  32957  cvlsupr2  32980  cvrexchlem  33055  cvratlem  33057  atcvrj0  33064  cvrat4  33079  cvrat42  33080  4noncolr3  33089  ps-1  33113  llnnlt  33159  lplnnlt  33201  lvolnltN  33254  dalempnes  33287  dalemqnet  33288  dalem-cly  33307  dalem44  33352  pmaple  33397  cdlemblem  33429  paddss  33481  2polcon4bN  33554  ltrneq2  33784  cdlemc3  33830  cdleme11h  33903  cdleme16b  33916  cdlemednpq  33936  tendospcanN  34662  dihmeetlem13N  34958  mapdordlem2  35276  mapdn0  35308  ctbnfien  35732  rmxypairf1o  35830  monotoddzzfi  35861  oddcomabszz  35863  acongtr  35899  frege124d  36424  expgrowth  36754  sbcbi  36970  csbeq2gOLD  36986  funressnfv  38774  iccpartnel  38897  2elfz2melfz  39203  red1wlklem  39867  red1wlk  39868  crctcsh1wlkn0lem3  39990  crctcsh1wlkn0lem5  39992  uzlidlring  40437  ply1mulgsumlem2  40687  fllog2  40887  dignn0flhalflem1  40934
  Copyright terms: Public domain W3C validator