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

Theorem sylibd 240
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 230 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 47 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  3imtr3d  294  ceqsalt  3525  sbceqal  3832  csbiebt  3909  rspcsbela  4384  sneqrg  4762  preq1b  4769  csbexg  5205  elrnrexdm  6847  isoselem  7083  riotass2  7133  ordzsl  7549  oaword2  8168  oaordex  8173  omword1  8188  om00  8190  omeulem2  8198  oen0  8201  oeeui  8217  nnaordex  8253  php3  8691  onomeneq  8696  frfi  8751  infglb  8942  suc11reg  9070  cardne  9382  cardsdomel  9391  carduni  9398  acndom  9465  alephinit  9509  cfflb  9669  cfslb2n  9678  fin23lem28  9750  isf34lem6  9790  fin1a2lem9  9818  axcc3  9848  winalim2  10106  inar1  10185  rankcf  10187  addclprlem2  10427  mulclprlem  10429  ltexprlem7  10452  prlem936  10457  reclem4pr  10460  sqgt0sr  10516  ltord2  11157  leord2  11158  eqord2  11159  mulgt1  11487  mulge0b  11498  fiminreOLD  11578  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  12977  uznfz  12978  axdc4uzlem  13339  facndiv  13636  hashvnfin  13709  hashgt12el  13771  hashgt12el2  13772  hashf1  13803  ccatalpha  13935  swrdccatin2  14079  swrdccatin2d  14094  rennim  14586  cau3lem  14702  caubnd2  14705  o1lo1  14882  climrlim2  14892  climshft  14921  subcn2  14939  mulcn2  14940  rlimo1  14961  o1dif  14974  isercoll  15012  caucvgrlem  15017  serf0  15025  cvgrat  15227  efieq1re  15540  moddvds  15606  dvdsssfz1  15656  smuval2  15819  nn0seqcvgd  15902  algcvgblem  15909  eucalglt  15917  lcmgcdlem  15938  rpmul  15991  divgcdcoprm0  15997  isprm6  16046  rpexp  16052  eulerthlem2  16107  prmdiv  16110  pcprendvds2  16166  pcz  16205  pcprmpw  16207  pcadd2  16214  pcfac  16223  expnprm  16226  ramlb  16343  firest  16694  joineu  17608  meeteu  17622  latjlej1  17663  latjlej2  17664  latmlem1  17679  latmlem2  17680  lubun  17721  acsmapd  17776  imasgrp2  18152  issubg4  18236  psgnunilem4  18554  oddvdsnn0  18601  odmulgeq  18613  subgpgp  18651  odcau  18658  lsmlub  18719  frgpnabllem1  18922  pgpfac1lem2  19126  pgpfac1lem3a  19127  pgpfac1lem3  19128  irredrmul  19386  islmhm2  19739  lsmelval2  19786  lspsnat  19846  znidomb  20636  ip2eq  20725  lsmcss  20764  cnpnei  21800  cncls2  21809  cncls  21810  cnntr  21811  cnt0  21882  isnrm2  21894  comppfsc  22068  kqcldsat  22269  isr0  22273  hmeoopn  22302  hmeocld  22303  trufil  22446  opnsubg  22643  ghmcnp  22650  tgphaus  22652  qustgpopn  22655  tsmsgsum  22674  isngp4  23148  xrhmeo  23477  bndth  23489  cfilres  23826  caubl  23838  ivthlem2  23980  ovolicc2  24050  ismbf3d  24182  itg1ge0a  24239  mbfi1flim  24251  itg2gt0  24288  dvge0  24530  dvcnvrelem1  24541  dvcvx  24544  mdegmullem  24599  ig1peu  24692  plyco  24758  coemulc  24772  dgreq0  24782  dgrlt  24783  plymul0or  24797  plydiveu  24814  quotcan  24825  aalioulem3  24850  ulmcaulem  24909  sincosq3sgn  25013  sincosq4sgn  25014  sineq0  25036  logrec  25268  xrlimcnp  25473  cxploglim  25482  lgamgulmlem1  25533  mumul  25685  chtub  25715  perfect1  25731  dchrelbas3  25741  lgsdir2lem4  25831  lgsne0  25838  lgsquad2lem2  25888  2sqlem8a  25928  2sqblem  25934  axcontlem2  26678  elntg2  26698  redwlklem  27380  redwlk  27381  crctcshwlkn0lem3  27517  crctcshwlkn0lem5  27519  clwwlkext2edg  27762  wwlksubclwwlk  27764  frgrwopregasn  28022  frgrwopregbsn  28023  blocnilem  28508  ip2eqi  28560  ubthlem2  28575  hial0  28806  hial02  28807  hial2eq  28810  h1datomi  29285  sumspansn  29353  lnopcnbd  29740  riesz4i  29767  bra11  29812  pjss2coi  29868  pjnormssi  29872  pjorthcoi  29873  pjclem4a  29902  pj3lem1  29910  pj3cor1i  29913  hst1h  29931  stm1i  29947  strlem1  29954  golem2  29976  mdbr2  30000  dmdbr5  30012  mdsl2i  30026  atexch  30085  atcvatlem  30089  chirredlem1  30094  cdjreui  30136  cdj1i  30137  cdj3lem1  30138  xraddge02  30406  submarchi  30742  isarchiofld  30817  esumcvg  31244  bnj1468  32017  loop1cycl  32281  erdsze2lem2  32348  funeldmb  32903  btwnexch  33383  btwncolinear2  33428  btwncolinear3  33429  btwncolinear4  33430  btwncolinear5  33431  btwncolinear6  33432  nn0prpw  33568  cldbnd  33571  onsuct0  33686  onint1  33694  bj-ceqsalt0  34097  bj-ceqsalt1  34098  bj-inftyexpiinj  34383  bj-bary1lem1  34480  bj-bary1  34481  relowlssretop  34526  isinf2  34568  ltflcei  34761  tan2h  34765  poimirlem26  34799  poimirlem31  34804  ftc1anclem6  34853  dvasin  34859  dvacos  34860  fdc  34901  caushft  34917  heibor1lem  34968  bfplem2  34982  rrncmslem  34991  rngosn3  35083  mpobi123f  35321  riotasv3d  35976  lsatcv1  36064  lub0N  36205  glb0N  36209  oplecon3b  36216  cmtbr4N  36271  cvrnbtwn2  36291  atnlt  36329  atlatle  36336  cvlsupr2  36359  cvrexchlem  36435  cvratlem  36437  atcvrj0  36444  cvrat4  36459  cvrat42  36460  4noncolr3  36469  ps-1  36493  llnnlt  36539  lplnnlt  36581  lvolnltN  36634  dalempnes  36667  dalemqnet  36668  dalem-cly  36687  dalem44  36732  pmaple  36777  cdlemblem  36809  paddss  36861  2polcon4bN  36934  ltrneq2  37164  cdlemc3  37209  cdleme11h  37282  cdleme16b  37295  cdlemednpq  37315  tendospcanN  38039  dihmeetlem13N  38335  mapdordlem2  38653  mapdn0  38685  ccatcan2d  39005  ctbnfien  39293  rmxypairf1o  39386  monotoddzzfi  39417  oddcomabszz  39419  acongtr  39453  frege124d  39984  expgrowth  40544  sbcbi  40750  limsupmnflem  41877  funressnfv  43155  2elfz2melfz  43395  iccpartnel  43475  requad2  43665  uzlidlring  44128  ply1mulgsumlem2  44369  fllog2  44556  dignn0flhalflem1  44603
  Copyright terms: Public domain W3C validator