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

Theorem sylibd 229
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 219 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 47 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  3imtr3d  282  ceqsalt  3259  sbceqal  3520  csbiebt  3586  rspcsbela  4039  sneqrg  4402  preq1b  4409  csbexg  4825  elrnrexdm  6403  isoselem  6631  riotass2  6678  ordzsl  7087  oaword2  7678  oaordex  7683  omword1  7698  om00  7700  omeulem2  7708  oen0  7711  oeeui  7727  nnaordex  7763  php3  8187  onomeneq  8191  frfi  8246  infglb  8437  suc11reg  8554  cardne  8829  cardsdomel  8838  carduni  8845  acndom  8912  alephinit  8956  cfflb  9119  cfslb2n  9128  fin23lem28  9200  isf34lem6  9240  fin1a2lem9  9268  axcc3  9298  winalim2  9556  inar1  9635  rankcf  9637  addclprlem2  9877  mulclprlem  9879  ltexprlem7  9902  prlem936  9907  reclem4pr  9910  sqgt0sr  9965  ltord2  10595  leord2  10596  eqord2  10597  mulgt1  10920  mulge0b  10931  fiminre  11010  lt2halves  11305  addltmul  11306  ltsubnn0  11382  nzadd  11463  zextlt  11489  recnz  11490  zeo  11501  peano5uzi  11504  uzm1  11756  irradd  11850  irrmul  11851  xltneg  12086  xleadd1  12123  xmulasslem  12153  xlemul1a  12156  xlemul1  12158  fznuz  12460  uznfz  12461  axdc4uzlem  12822  facndiv  13115  hashvnfin  13189  hashgt12el  13248  hashgt12el2  13249  hashf1  13279  ccatalpha  13411  swrdccatin2  13533  swrdccatin2d  13546  swrdccatin12d  13547  rennim  14023  cau3lem  14138  caubnd2  14141  o1lo1  14312  climrlim2  14322  climshft  14351  subcn2  14369  mulcn2  14370  rlimo1  14391  o1dif  14404  isercoll  14442  caucvgrlem  14447  serf0  14455  cvgrat  14659  efieq1re  14973  moddvds  15038  dvdsssfz1  15087  smuval2  15251  nn0seqcvgd  15330  algcvgblem  15337  eucalglt  15345  lcmgcdlem  15366  coprmdvdsOLD  15414  rpmul  15420  divgcdcoprm0  15426  isprm6  15473  rpexp  15479  eulerthlem2  15534  prmdiv  15537  pcprendvds2  15593  pcz  15632  pcprmpw  15634  pcadd2  15641  pcfac  15650  expnprm  15653  ramlb  15770  firest  16140  joineu  17057  meeteu  17071  latjlej1  17112  latjlej2  17113  latmlem1  17128  latmlem2  17129  lubun  17170  acsmapd  17225  imasgrp2  17577  issubg4  17660  psgnunilem4  17963  oddvdsnn0  18009  odmulgeq  18020  subgpgp  18058  odcau  18065  lsmlub  18124  frgpnabllem1  18322  pgpfac1lem2  18520  pgpfac1lem3a  18521  pgpfac1lem3  18522  irredrmul  18753  islmhm2  19086  lsmelval2  19133  lspsnat  19193  znidomb  19958  ip2eq  20046  lsmcss  20084  cnpnei  21116  cncls2  21125  cncls  21126  cnntr  21127  cnt0  21198  isnrm2  21210  comppfsc  21383  kqcldsat  21584  isr0  21588  hmeoopn  21617  hmeocld  21618  trufil  21761  opnsubg  21958  ghmcnp  21965  tgphaus  21967  qustgpopn  21970  tsmsgsum  21989  isngp4  22463  xrhmeo  22792  bndth  22804  cfilres  23140  caubl  23152  ivthlem2  23267  ovolicc2  23336  ismbf3d  23466  itg1ge0a  23523  mbfi1flim  23535  itg2gt0  23572  dvge0  23814  dvcnvrelem1  23825  dvcvx  23828  mdegmullem  23883  ig1peu  23976  plyco  24042  coemulc  24056  dgreq0  24066  dgrlt  24067  plymul0or  24081  plydiveu  24098  quotcan  24109  aalioulem3  24134  ulmcaulem  24193  sincosq3sgn  24297  sincosq4sgn  24298  sineq0  24318  logrec  24546  xrlimcnp  24740  cxploglim  24749  lgamgulmlem1  24800  mumul  24952  chtub  24982  perfect1  24998  dchrelbas3  25008  lgsdir2lem4  25098  lgsne0  25105  lgsquad2lem2  25155  2sqlem8a  25195  2sqblem  25201  axcontlem2  25890  redwlklem  26624  redwlk  26625  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  clwwlkext2edg  27020  wwlksubclwwlk  27023  clwlksf1clwwlklem  27055  frgrwopregasn  27296  frgrwopregbsn  27297  blocnilem  27787  ip2eqi  27840  ubthlem2  27855  hial0  28087  hial02  28088  hial2eq  28091  h1datomi  28568  sumspansn  28636  lnopcnbd  29023  riesz4i  29050  bra11  29095  pjss2coi  29151  pjnormssi  29155  pjorthcoi  29156  pjclem4a  29185  pj3lem1  29193  pj3cor1i  29196  hst1h  29214  stm1i  29230  strlem1  29237  golem2  29259  mdbr2  29283  dmdbr5  29295  mdsl2i  29309  atexch  29368  atcvatlem  29372  chirredlem1  29377  cdjreui  29419  cdj1i  29420  cdj3lem1  29421  xraddge02  29649  submarchi  29868  isarchiofld  29945  esumcvg  30276  bnj1468  31042  erdsze2lem2  31312  funeldmb  31787  btwnexch  32257  btwncolinear2  32302  btwncolinear3  32303  btwncolinear4  32304  btwncolinear5  32305  btwncolinear6  32306  nn0prpw  32443  cldbnd  32446  onsuct0  32565  onint1  32573  bj-ceqsalt0  32998  bj-ceqsalt1  32999  bj-inftyexpiinj  33226  bj-bary1lem1  33291  bj-bary1  33292  relowlssretop  33341  ltflcei  33527  tan2h  33531  poimirlem26  33565  poimirlem31  33570  ftc1anclem6  33620  dvasin  33626  dvacos  33627  fdc  33671  caushft  33687  heibor1lem  33738  bfplem2  33752  rrncmslem  33761  rngosn3  33853  mpt2bi123f  34101  riotasv3d  34564  lsatcv1  34653  lub0N  34794  glb0N  34798  oplecon3b  34805  cmtbr4N  34860  cvrnbtwn2  34880  atnlt  34918  atlatle  34925  cvlsupr2  34948  cvrexchlem  35023  cvratlem  35025  atcvrj0  35032  cvrat4  35047  cvrat42  35048  4noncolr3  35057  ps-1  35081  llnnlt  35127  lplnnlt  35169  lvolnltN  35222  dalempnes  35255  dalemqnet  35256  dalem-cly  35275  dalem44  35320  pmaple  35365  cdlemblem  35397  paddss  35449  2polcon4bN  35522  ltrneq2  35752  cdlemc3  35798  cdleme11h  35871  cdleme16b  35884  cdlemednpq  35904  tendospcanN  36629  dihmeetlem13N  36925  mapdordlem2  37243  mapdn0  37275  ctbnfien  37699  rmxypairf1o  37793  monotoddzzfi  37824  oddcomabszz  37826  acongtr  37862  frege124d  38370  expgrowth  38851  sbcbi  39066  csbeq2gOLD  39082  limsupmnflem  40270  funressnfv  41529  2elfz2melfz  41653  iccpartnel  41699  uzlidlring  42254  ply1mulgsumlem2  42500  fllog2  42687  dignn0flhalflem1  42734
  Copyright terms: Public domain W3C validator