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

Theorem sylibd 228
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylibd.1 (𝜑 → (𝜓𝜒))
sylibd.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
sylibd (𝜑 → (𝜓𝜃))

Proof of Theorem sylibd
StepHypRef Expression
1 sylibd.1 . 2 (𝜑 → (𝜓𝜒))
2 sylibd.2 . . 3 (𝜑 → (𝜒𝜃))
32biimpd 218 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 46 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  3imtr3d  281  ceqsalt  3201  sbceqal  3454  csbiebt  3519  rspcsbela  3958  sneqrg  4306  preq1b  4313  csbexg  4715  elrnrexdm  6256  isoselem  6469  riotass2  6515  ordzsl  6915  oaword2  7498  oaordex  7503  omword1  7518  om00  7520  omeulem2  7528  oen0  7531  oeeui  7547  nnaordex  7583  php3  8009  onomeneq  8013  frfi  8068  infglb  8257  suc11reg  8377  cardne  8652  cardsdomel  8661  carduni  8668  acndom  8735  alephinit  8779  cfflb  8942  cfslb2n  8951  fin23lem28  9023  isf34lem6  9063  fin1a2lem9  9091  axcc3  9121  winalim2  9375  inar1  9454  rankcf  9456  addclprlem2  9696  mulclprlem  9698  ltexprlem7  9721  prlem936  9726  reclem4pr  9729  sqgt0sr  9784  ltord2  10409  leord2  10410  eqord2  10411  mulgt1  10734  mulge0b  10745  fiminre  10824  lt2halves  11117  addltmul  11118  ltsubnn0  11194  nzadd  11261  zextlt  11286  recnz  11287  zeo  11298  peano5uzi  11301  uzm1  11553  irradd  11647  irrmul  11648  xltneg  11884  xleadd1  11917  xmulasslem  11947  xlemul1a  11950  xlemul1  11952  fznuz  12249  uznfz  12250  axdc4uzlem  12602  facndiv  12895  hashvnfin  12967  hashgt12el  13025  hashgt12el2  13026  hashf1  13053  ccatalpha  13177  swrdccatin2  13287  swrdccatin2d  13300  swrdccatin12d  13301  rennim  13776  cau3lem  13891  caubnd2  13894  o1lo1  14065  climrlim2  14075  climshft  14104  subcn2  14122  mulcn2  14123  rlimo1  14144  o1dif  14157  isercoll  14195  caucvgrlem  14200  serf0  14208  cvgrat  14403  efieq1re  14717  moddvds  14778  dvdsssfz1  14827  smuval2  14991  nn0seqcvgd  15070  algcvgblem  15077  eucalglt  15085  lcmgcdlem  15106  coprmdvdsOLD  15154  rpmul  15160  divgcdcoprm0  15166  isprm6  15213  rpexp  15219  eulerthlem2  15274  prmdiv  15277  pcprendvds2  15333  pcz  15372  pcprmpw  15374  pcadd2  15381  pcfac  15390  expnprm  15393  ramlb  15510  firest  15865  joineu  16782  meeteu  16796  latjlej1  16837  latjlej2  16838  latmlem1  16853  latmlem2  16854  lubun  16895  acsmapd  16950  imasgrp2  17302  issubg4  17385  psgnunilem4  17689  oddvdsnn0  17735  odmulgeq  17746  subgpgp  17784  odcau  17791  lsmlub  17850  frgpnabllem1  18048  pgpfac1lem2  18246  pgpfac1lem3a  18247  pgpfac1lem3  18248  irredrmul  18479  islmhm2  18808  lsmelval2  18855  lspsnat  18915  znidomb  19677  ip2eq  19765  lsmcss  19803  cnpnei  20826  cncls2  20835  cncls  20836  cnntr  20837  cnt0  20908  isnrm2  20920  comppfsc  21093  kqcldsat  21294  isr0  21298  hmeoopn  21327  hmeocld  21328  trufil  21472  opnsubg  21669  ghmcnp  21676  tgphaus  21678  qustgpopn  21681  tsmsgsum  21700  isngp4  22174  xrhmeo  22501  bndth  22513  cfilres  22847  caubl  22859  ivthlem2  22973  ovolicc2  23042  ismbf3d  23172  itg1ge0a  23229  mbfi1flim  23241  itg2gt0  23278  dvge0  23518  dvcnvrelem1  23529  dvcvx  23532  mdegmullem  23587  ig1peu  23680  plyco  23746  coemulc  23760  dgreq0  23770  dgrlt  23771  plymul0or  23785  plydiveu  23802  quotcan  23813  aalioulem3  23838  ulmcaulem  23897  sincosq3sgn  24001  sincosq4sgn  24002  sineq0  24022  logrec  24246  xrlimcnp  24440  cxploglim  24449  lgamgulmlem1  24500  mumul  24652  chtub  24682  perfect1  24698  dchrelbas3  24708  lgsdir2lem4  24798  lgsne0  24805  lgsquad2lem2  24855  2sqlem8a  24895  2sqblem  24901  axcontlem2  25591  cusgrarn  25782  redwlk  25930  wlkdvspth  25932  wlkiswwlk1  26012  wlklniswwlkn1  26021  clwwlkext2edg  26124  wwlksubclwwlk  26126  clwlkf1clwwlklem  26170  frgrawopreg1  26371  frgrawopreg2  26372  extwwlkfablem2  26399  blocnilem  26837  ip2eqi  26890  ubthlem2  26905  hial0  27137  hial02  27138  hial2eq  27141  h1datomi  27618  sumspansn  27686  lnopcnbd  28073  riesz4i  28100  bra11  28145  pjss2coi  28201  pjnormssi  28205  pjorthcoi  28206  pjclem4a  28235  pj3lem1  28243  pj3cor1i  28246  hst1h  28264  stm1i  28280  strlem1  28287  golem2  28309  mdbr2  28333  dmdbr5  28345  mdsl2i  28359  atexch  28418  atcvatlem  28422  chirredlem1  28427  cdjreui  28469  cdj1i  28470  cdj3lem1  28471  xraddge02  28705  submarchi  28865  isarchiofld  28942  esumcvg  29269  bnj1468  29964  erdsze2lem2  30234  btwnexch  31096  btwncolinear2  31141  btwncolinear3  31142  btwncolinear4  31143  btwncolinear5  31144  btwncolinear6  31145  nn0prpw  31282  cldbnd  31285  onsuct0  31404  onint1  31412  bj-ceqsalt0  31861  bj-ceqsalt1  31862  bj-inftyexpiinj  32067  bj-bary1lem1  32132  bj-bary1  32133  relowlssretop  32181  ltflcei  32361  tan2h  32365  poimirlem26  32399  poimirlem31  32404  ftc1anclem6  32454  dvasin  32460  dvacos  32461  fdc  32505  caushft  32521  heibor1lem  32572  bfplem2  32586  rrncmslem  32595  rngosn3  32687  mpt2bi123f  32935  riotasv3d  33058  lsatcv1  33147  lub0N  33288  glb0N  33292  oplecon3b  33299  cmtbr4N  33354  cvrnbtwn2  33374  atnlt  33412  atlatle  33419  cvlsupr2  33442  cvrexchlem  33517  cvratlem  33519  atcvrj0  33526  cvrat4  33541  cvrat42  33542  4noncolr3  33551  ps-1  33575  llnnlt  33621  lplnnlt  33663  lvolnltN  33716  dalempnes  33749  dalemqnet  33750  dalem-cly  33769  dalem44  33814  pmaple  33859  cdlemblem  33891  paddss  33943  2polcon4bN  34016  ltrneq2  34246  cdlemc3  34292  cdleme11h  34365  cdleme16b  34378  cdlemednpq  34398  tendospcanN  35124  dihmeetlem13N  35420  mapdordlem2  35738  mapdn0  35770  ctbnfien  36194  rmxypairf1o  36288  monotoddzzfi  36319  oddcomabszz  36321  acongtr  36357  frege124d  36866  expgrowth  37350  sbcbi  37564  csbeq2gOLD  37580  funressnfv  39651  iccpartnel  39771  2elfz2melfz  40172  red1wlklem  40872  red1wlk  40873  crctcsh1wlkn0lem3  41007  crctcsh1wlkn0lem5  41009  clwwlksext2edg  41222  wwlksubclwwlks  41224  clwlksf1clwwlklem  41267  frgrwopreg1  41479  frgrwopreg2  41480  av-extwwlkfablem2  41502  uzlidlring  41711  ply1mulgsumlem2  41961  fllog2  42152  dignn0flhalflem1  42199
  Copyright terms: Public domain W3C validator