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

Theorem sylibd 242
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 232 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 47 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  3imtr3d  296  ceqsalt  3474  sbceqal  3782  csbiebt  3857  rspcsbela  4343  sneqrg  4730  preq1b  4737  csbexg  5178  elrnrexdm  6832  isoselem  7073  riotass2  7123  ordzsl  7540  oaword2  8162  oaordex  8167  omword1  8182  om00  8184  omeulem2  8192  oen0  8195  oeeui  8211  nnaordex  8247  php3  8687  onomeneq  8693  frfi  8747  infglb  8938  suc11reg  9066  cardne  9378  cardsdomel  9387  carduni  9394  acndom  9462  alephinit  9506  cfflb  9670  cfslb2n  9679  fin23lem28  9751  isf34lem6  9791  fin1a2lem9  9819  axcc3  9849  winalim2  10107  inar1  10186  rankcf  10188  addclprlem2  10428  mulclprlem  10430  ltexprlem7  10453  prlem936  10458  reclem4pr  10461  sqgt0sr  10517  ltord2  11158  leord2  11159  eqord2  11160  mulgt1  11488  mulge0b  11499  lt2halves  11860  addltmul  11861  ltsubnn0  11936  nzadd  12018  zextlt  12044  recnz  12045  zeo  12056  peano5uzi  12059  uzm1  12264  irradd  12360  irrmul  12361  xltneg  12598  xleadd1  12636  xmulasslem  12666  xlemul1a  12669  xlemul1  12671  fznuz  12984  uznfz  12985  axdc4uzlem  13346  facndiv  13644  hashvnfin  13717  hashgt12el  13779  hashgt12el2  13780  hashf1  13811  ccatalpha  13938  swrdccatin2  14082  swrdccatin2d  14097  rennim  14590  cau3lem  14706  caubnd2  14709  o1lo1  14886  climrlim2  14896  climshft  14925  subcn2  14943  mulcn2  14944  rlimo1  14965  o1dif  14978  isercoll  15016  caucvgrlem  15021  serf0  15029  cvgrat  15231  efieq1re  15544  moddvds  15610  dvdsssfz1  15660  smuval2  15821  nn0seqcvgd  15904  algcvgblem  15911  eucalglt  15919  lcmgcdlem  15940  rpmul  15993  divgcdcoprm0  15999  isprm6  16048  rpexp  16054  eulerthlem2  16109  prmdiv  16112  pcprendvds2  16168  pcz  16207  pcprmpw  16209  pcadd2  16216  pcfac  16225  expnprm  16228  ramlb  16345  firest  16698  joineu  17612  meeteu  17626  latjlej1  17667  latjlej2  17668  latmlem1  17683  latmlem2  17684  lubun  17725  acsmapd  17780  imasgrp2  18206  issubg4  18290  psgnunilem4  18617  oddvdsnn0  18664  odmulgeq  18676  subgpgp  18714  odcau  18721  lsmlub  18782  frgpnabllem1  18986  pgpfac1lem2  19190  pgpfac1lem3a  19191  pgpfac1lem3  19192  irredrmul  19453  islmhm2  19803  lsmelval2  19850  lspsnat  19910  znidomb  20253  ip2eq  20342  lsmcss  20381  cnpnei  21869  cncls2  21878  cncls  21879  cnntr  21880  cnt0  21951  isnrm2  21963  comppfsc  22137  kqcldsat  22338  isr0  22342  hmeoopn  22371  hmeocld  22372  trufil  22515  opnsubg  22713  ghmcnp  22720  tgphaus  22722  qustgpopn  22725  tsmsgsum  22744  isngp4  23218  xrhmeo  23551  bndth  23563  cfilres  23900  caubl  23912  ivthlem2  24056  ovolicc2  24126  ismbf3d  24258  itg1ge0a  24315  mbfi1flim  24327  itg2gt0  24364  dvge0  24609  dvcnvrelem1  24620  dvcvx  24623  mdegmullem  24679  ig1peu  24772  plyco  24838  coemulc  24852  dgreq0  24862  dgrlt  24863  plymul0or  24877  plydiveu  24894  quotcan  24905  aalioulem3  24930  ulmcaulem  24989  sincosq3sgn  25093  sincosq4sgn  25094  sineq0  25116  logrec  25349  xrlimcnp  25554  cxploglim  25563  lgamgulmlem1  25614  mumul  25766  chtub  25796  perfect1  25812  dchrelbas3  25822  lgsdir2lem4  25912  lgsne0  25919  lgsquad2lem2  25969  2sqlem8a  26009  2sqblem  26015  axcontlem2  26759  elntg2  26779  redwlklem  27461  redwlk  27462  crctcshwlkn0lem3  27598  crctcshwlkn0lem5  27600  clwwlkext2edg  27841  wwlksubclwwlk  27843  frgrwopregasn  28101  frgrwopregbsn  28102  blocnilem  28587  ip2eqi  28639  ubthlem2  28654  hial0  28885  hial02  28886  hial2eq  28889  h1datomi  29364  sumspansn  29432  lnopcnbd  29819  riesz4i  29846  bra11  29891  pjss2coi  29947  pjnormssi  29951  pjorthcoi  29952  pjclem4a  29981  pj3lem1  29989  pj3cor1i  29992  hst1h  30010  stm1i  30026  strlem1  30033  golem2  30055  mdbr2  30079  dmdbr5  30091  mdsl2i  30105  atexch  30164  atcvatlem  30168  chirredlem1  30173  cdjreui  30215  cdj1i  30216  cdj3lem1  30217  xraddge02  30506  submarchi  30865  isarchiofld  30941  esumcvg  31455  bnj1468  32228  loop1cycl  32497  erdsze2lem2  32564  funeldmb  33119  btwnexch  33599  btwncolinear2  33644  btwncolinear3  33645  btwncolinear4  33646  btwncolinear5  33647  btwncolinear6  33648  nn0prpw  33784  cldbnd  33787  onsuct0  33902  onint1  33910  bj-ceqsalt0  34324  bj-ceqsalt1  34325  bj-inftyexpiinj  34624  bj-bary1lem1  34725  bj-bary1  34726  relowlssretop  34780  isinf2  34822  ltflcei  35045  tan2h  35049  poimirlem26  35083  poimirlem31  35088  ftc1anclem6  35135  dvasin  35141  dvacos  35142  fdc  35183  caushft  35199  heibor1lem  35247  bfplem2  35261  rrncmslem  35270  rngosn3  35362  mpobi123f  35600  riotasv3d  36256  lsatcv1  36344  lub0N  36485  glb0N  36489  oplecon3b  36496  cmtbr4N  36551  cvrnbtwn2  36571  atnlt  36609  atlatle  36616  cvlsupr2  36639  cvrexchlem  36715  cvratlem  36717  atcvrj0  36724  cvrat4  36739  cvrat42  36740  4noncolr3  36749  ps-1  36773  llnnlt  36819  lplnnlt  36861  lvolnltN  36914  dalempnes  36947  dalemqnet  36948  dalem-cly  36967  dalem44  37012  pmaple  37057  cdlemblem  37089  paddss  37141  2polcon4bN  37214  ltrneq2  37444  cdlemc3  37489  cdleme11h  37562  cdleme16b  37575  cdlemednpq  37595  tendospcanN  38319  dihmeetlem13N  38615  mapdordlem2  38933  mapdn0  38965  ccatcan2d  39420  ctbnfien  39757  rmxypairf1o  39850  monotoddzzfi  39881  oddcomabszz  39883  acongtr  39917  frege124d  40460  expgrowth  41037  sbcbi  41243  limsupmnflem  42360  funressnfv  43633  2elfz2melfz  43873  iccpartnel  43953  requad2  44139  uzlidlring  44551  ply1mulgsumlem2  44793  fllog2  44980  dignn0flhalflem1  45027
  Copyright terms: Public domain W3C validator