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

Theorem syld 47
Description: Syllogism deduction. Deduction associated with syl 17. See conventions 27228 for the meaning of "associated deduction" or "deduction form". (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
Hypotheses
Ref Expression
syld.1 (𝜑 → (𝜓𝜒))
syld.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
syld (𝜑 → (𝜓𝜃))

Proof of Theorem syld
StepHypRef Expression
1 syld.1 . 2 (𝜑 → (𝜓𝜒))
2 syld.2 . . 3 (𝜑 → (𝜒𝜃))
32a1d 25 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpdd 43 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syldc  48  3syld  60  sylsyld  61  nsyld  154  pm2.61d  170  sylibd  229  sylbid  230  sylibrd  249  sylbird  250  syland  498  ax12v2  2047  ax12vOLD  2048  ax12vOLDOLD  2049  alrimdd  2081  axc16g  2132  axc16nf  2135  axc11rvOLD  2138  axc11r  2185  alrimddOLD  2193  nfeqf2  2295  sbequi  2373  2eu1  2551  axext3  2602  trel3  4751  poss  5027  sess2  5073  wefrc  5098  wereu2  5101  funun  5920  ssimaex  6250  f1cofveqaeq  6500  f1imass  6506  soisoi  6563  isores3  6570  isofrlem  6575  isoselem  6576  weniso  6589  abnexg  6949  oninton  6985  orduniorsuc  7015  limuni3  7037  tfindsg  7045  limom  7065  f1o2ndf1  7270  soxp  7275  extmptsuppeq  7304  smoel  7442  tfrlem9  7466  tz7.49  7525  seqomlem1  7530  odi  7644  omass  7645  omeulem2  7648  oeordsuc  7659  oeeulem  7666  ertr  7742  swoord2  7759  ecopovtrn  7835  domtriord  8091  onomeneq  8135  unxpdomlem2  8150  isinf  8158  pssnn  8163  findcard3  8188  frfi  8190  unblem3  8199  dffi3  8322  en3lplem1  8496  inf3lem5  8514  cantnfle  8553  cantnfp1lem3  8562  rankxpsuc  8730  tcrank  8732  ficardom  8772  carduni  8792  infxpenlem  8821  dfac8alem  8837  ac10ct  8842  ween  8843  alephdom  8889  alephle  8896  iscard3  8901  alephfp  8916  cdainf  8999  pwsdompw  9011  infdif  9016  cfslbn  9074  cofsmo  9076  cfcof  9081  fin1a2s  9221  domtriomlem  9249  ac6num  9286  zorn2lem3  9305  axdclem2  9327  imadomg  9341  iundom2g  9347  ficard  9372  fpwwe2lem8  9444  fpwwe2  9450  gchaclem  9485  tskr1om2  9575  inar1  9582  tskord  9587  tskuni  9590  grudomon  9624  grur1a  9626  grur1  9627  addnidpi  9708  ltexnq  9782  genpnnp  9812  addclprlem2  9824  mulclprlem  9826  psslinpr  9838  ltexprlem6  9848  ltexprlem7  9849  addcanpr  9853  mulgt0sr  9911  map2psrpr  9916  supsrlem  9917  axrrecex  9969  letr  10116  dedekind  10185  recex  10644  lemul12b  10865  mulgt1  10867  fimaxre2  10954  lbreu  10958  nnrecgt0  11043  nnunb  11273  bndndx  11276  zeo  11448  uzind  11454  fzind  11460  fnn0ind  11461  suprfinzcl  11477  suprzcl2  11763  zmax  11770  rpnnen1lem5  11803  rpnnen1lem5OLD  11809  xrletr  11974  qbtwnre  12015  qsqueeze  12017  qextltlem  12018  xralrple  12021  xlesubadd  12078  supxrunb1  12134  icoshft  12279  zltaddlt1le  12309  fzen  12343  elfz1b  12394  elfz0fzfz0  12428  elfzmlbp  12434  elfzo0z  12493  fzofzim  12498  fzo1fzo0n0  12502  elfzodifsumelfzo  12517  ssfzoulel  12546  modadd1  12690  modmul1  12706  uzrdgfni  12740  fsuppmapnn0fiub0  12776  fsuppmapnn0ub  12778  fsuppmapnn0fz  12779  seqcl2  12802  seqfveq2  12806  seqshft2  12810  monoord  12814  seqsplit  12817  seqf1olem1  12823  seqf1olem2  12824  seqid2  12830  seqhomo  12831  expnbnd  12976  faclbnd4lem4  13066  seqcoll  13231  hashle2pr  13242  elss2prb  13252  ccatalpha  13358  swrdsbslen  13430  swrdspsleq  13431  swrdswrdlem  13441  swrdswrd  13442  reuccats1lem  13461  swrdccatin12lem2a  13466  swrdccatin12lem2b  13467  swrdccatin12lem3  13471  swrdccat3a  13475  swrdccat3blem  13476  repswswrd  13512  cshf1  13537  swrd2lsw  13676  sqeqd  13887  sqrmo  13973  cau3lem  14075  icodiamlt  14155  limsupbnd2  14195  lo1bdd2  14236  climuni  14264  rlimcn2  14302  mulcn2  14307  o1of2  14324  rlimo1  14328  lo1le  14363  isercolllem1  14376  iseralt  14396  cvgrat  14596  fprodss  14659  znnenlem  14921  rpnnen2lem12  14935  ruclem3  14943  sqrt2irr  14960  dvds2lem  14975  dvdslelem  15012  dvdsabseq  15016  divalglem8  15104  bitsinv1lem  15144  sadcaddlem  15160  smu01lem  15188  smueqlem  15193  bezoutlem4  15240  dfgcd2  15244  algcvga  15273  lcmfunsnlem1  15331  lcmfunsnlem2lem1  15332  lcmfunsnlem2lem2  15333  lcmfdvdsb  15337  coprmgcdb  15343  coprmdvds2  15349  coprmprod  15356  isprm3  15377  prmdvdsfz  15398  isprm5  15400  coprm  15404  rpexp12i  15415  phibndlem  15456  dfphi2  15460  eulerthlem2  15468  odzdvds  15481  iserodd  15521  pclem  15524  pcpremul  15529  pcqcl  15542  pcdvdsb  15554  pcprmpw2  15567  difsqpwdvds  15572  pcaddlem  15573  pcmptcl  15576  pcfac  15584  prmpwdvds  15589  unbenlem  15593  prmreclem1  15601  4sqlem17  15646  vdwmc2  15664  vdwlem9  15674  vdwlem10  15675  vdwlem13  15678  vdwnnlem3  15682  ramcl  15714  prmgaplem7  15742  mreiincl  16237  initoid  16636  termoid  16637  initoeu2lem1  16645  pospo  16954  dirge  17218  gsmsymgrfixlem1  17828  oddvdsnn0  17944  oddvds  17947  odcl2  17963  gexdvds  17980  sylow1lem1  17994  sylow2alem2  18014  sylow2a  18015  efgi2  18119  efgsrel  18128  efgs1b  18130  cyggex2  18279  telgsums  18371  pgpfac1lem2  18455  pgpfac1lem3a  18456  pgpfac1lem3  18457  pgpfac1lem5  18459  lmodfopnelem2  18881  lssssr  18934  cply1mul  19645  gsummoncoe1  19655  gzrngunitlem  19792  znunit  19893  frgpcyg  19903  lsmcss  20017  obselocv  20053  obslbs  20055  cpmatacl  20502  cpmatinvcl  20503  cpmatmcllem  20504  m2cpminvid2lem  20540  mp2pm2mplem4  20595  pm2mp  20611  chfacfisf  20640  chfacfisfcpmat  20641  chfacfscmul0  20644  chfacfpmmul0  20648  cayhamlem4  20674  ordtrest2lem  20988  leordtval2  20997  lecldbas  21004  cncls  21059  cncnp  21065  cnpresti  21073  lmcnp  21089  cnt0  21131  isreg2  21162  cmpsublem  21183  cmpsub  21184  tgcmp  21185  bwth  21194  dfconn2  21203  1stcfb  21229  1stcelcls  21245  islly2  21268  dislly  21281  reftr  21298  comppfsc  21316  kgencn2  21341  txcnp  21404  txindis  21418  txcmplem1  21425  txlm  21432  xkohaus  21437  cnmptcom  21462  kqfvima  21514  isr0  21521  fgss2  21659  fbasrn  21669  filuni  21670  ufilmax  21692  isufil2  21693  cfinufil  21713  fmfnfmlem1  21739  fmfnfmlem2  21740  fmfnfmlem4  21742  fmfnfm  21743  fmco  21746  flimopn  21760  hausflim  21766  flimrest  21768  fclsopn  21799  flimfnfcls  21813  alexsubALTlem2  21833  alexsubALTlem3  21834  alexsubALT  21836  ptcmplem2  21838  cnextcn  21852  symgtgp  21886  qustgplem  21905  tsmsres  21928  tsmsxplem1  21937  isucn2  22064  imasdsf1olem  22159  bldisj  22184  blssps  22210  blss  22211  metcnp3  22326  ngptgp  22421  nrginvrcn  22477  nmoleub  22516  xrsmopn  22596  icccmplem3  22608  reconnlem2  22611  rectbntr0  22616  rescncf  22681  iocopnst  22720  iccpnfcnv  22724  lebnumii  22746  nmoleub2lem  22895  nmhmcn  22901  iscfil3  23052  iscau2  23056  iscau3  23057  iscau4  23058  iscmet3lem2  23071  cfilres  23075  caussi  23076  equivcfil  23078  equivcau  23079  ivthlem2  23202  ivthlem3  23203  ovoliunlem2  23252  ovoliunnul  23256  ovolicc2lem3  23268  ioombl1lem4  23310  dyadmax  23347  dyadmbl  23349  volsup2  23354  itg2le  23487  itg2const2  23489  itg2seq  23490  itgsplitioo  23585  dvnres  23675  rolle  23734  c1lip1  23741  dvivthlem1  23752  lhop1  23758  dvcnvrelem1  23761  dvfsumrlim  23775  ply1divmo  23876  ig1peu  23912  plypf1  23949  coeaddlem  23986  fta1  24044  quotcan  24045  aalioulem4  24071  ulmcaulem  24129  ulmcn  24134  pilem2  24187  sincosq1lem  24230  sinq12gt0  24240  sinq12ge0  24241  tanord1  24264  lognegb  24317  logrec  24482  dcubic  24554  xrlimcnp  24676  o1cxp  24682  ftalem2  24781  ftalem3  24782  fsumdvdscom  24892  chtub  24918  vmasum  24922  bcmono  24983  bposlem3  24992  bposlem7  24996  lgsdir  25038  lgsqrlem2  25053  lgsqrmodndvds  25059  lgsdchr  25061  gausslemma2dlem6  25078  gausslemma2d  25080  lgsquadlem2  25087  2lgslem3a1  25106  2lgslem3b1  25107  2lgslem3c1  25108  2lgslem3d1  25109  2sqlem6  25129  dchrisumlem3  25161  pntrsumbnd2  25237  pntpbnd1  25256  pntibnd  25263  pntlem3  25279  pntleml  25281  brbtwn2  25766  colinearalg  25771  axcontlem10  25834  edgupgr  26010  edglnl  26019  usgruspgrb  26057  subupgr  26160  uhgrspan1  26176  usgredgsscusgredg  26336  fusgrn0degnn0  26376  upgrewlkle2  26483  uspgr2wlkeq  26523  redwlk  26550  wlkdlem2  26561  upgrwlkdvdelem  26613  pthdlem1  26643  pthdlem2  26645  crctcshwlkn0lem3  26685  wlkiswwlks1  26734  wwlksm1edg  26748  wwlksnred  26768  wwlksnextbi  26770  umgr2adedgspth  26825  clwlkclwwlklem2fv2  26878  clwlkclwwlklem2a  26880  clwwlksf  26895  clwwlksext2edg  26903  wwlksubclwwlks  26905  clwwisshclwwslemlem  26906  eupth2lems  27078  frgrwopreglem4  27157  frgrregorufrg  27164  numclwwlkovf2ex  27191  numclwlk1lem2foa  27195  numclwlk1lem2fo  27199  ex-natded5.3-2  27235  isgrpo  27321  vacn  27519  ubthlem2  27697  htthlem  27744  normgt0  27954  shmodsi  28218  spansneleq  28399  h1datomi  28410  nmcexi  28855  pjnormssi  28997  stm1add3i  29076  golem2  29101  cvnsym  29119  dmdmd  29129  mdslmd1lem1  29154  mdslmd1i  29158  mdexchi  29164  atcveq0  29177  superpos  29183  hatomistici  29191  atoml2i  29212  atcvat2i  29216  chirredlem1  29219  atcvat3i  29225  mdsymlem3  29234  mdsymlem5  29236  cdj3lem2b  29266  cdj3i  29270  supssd  29461  infssd  29462  2sqmod  29622  resspos  29633  resstos  29634  submarchi  29714  tpr2rico  29932  ordtrest2NEWlem  29942  xrge0iifcnv  29953  omssubadd  30336  eulerpartlemb  30404  ballotlemfc0  30528  ballotlemfcc  30529  ftc2re  30650  subfacp1lem6  31141  iccllysconn  31206  cvmfolem  31235  cvmliftlem7  31247  cvmliftlem10  31250  fundmpss  31640  dfon2lem3  31664  dfon2lem6  31667  axext4dist  31680  trpredtr  31704  trpredmintr  31705  dftrpred3g  31707  trpredrec  31712  frmin  31713  soseq  31725  frrlem5e  31762  sltres  31789  nosepon  31792  nolesgn2o  31798  nodenselem8  31815  nosupbnd1lem1  31828  dfrdg4  32033  5segofs  32088  cgrextend  32090  segconeu  32093  btwncomim  32095  btwnswapid  32099  btwnintr  32101  btwnexch3  32102  btwndiff  32109  ifscgr  32126  cgrxfr  32137  btwnxfr  32138  lineext  32158  brofs2  32159  linecgr  32163  lineid  32165  idinside  32166  endofsegid  32167  btwnconn1lem13  32181  btwnconn3  32185  finminlem  32287  nn0prpwlem  32292  cldbnd  32296  clsint2  32299  fnessref  32327  neibastop3  32332  fgmin  32340  onsuct0  32415  limsucncmpi  32419  bj-axc14  32814  bj-restn0  33018  bj-0int  33030  wl-19.2reqv  33281  wl-aetr  33288  fin2so  33367  tan2h  33372  lindsenlbs  33375  poimirlem2  33382  poimirlem9  33389  poimirlem17  33397  poimirlem18  33398  poimirlem21  33401  poimirlem23  33403  poimirlem26  33406  poimirlem29  33409  poimirlem30  33410  poimirlem31  33411  poimir  33413  heicant  33415  mblfinlem2  33418  mblfinlem3  33419  itg2addnclem  33432  itg2addnclem2  33433  itg2gt0cn  33436  ftc1anclem5  33460  ftc1anclem6  33461  filbcmb  33506  nninfnub  33518  mettrifi  33524  geomcau  33526  istotbnd3  33541  sstotbnd2  33544  ismtybndlem  33576  heibor1lem  33579  heiborlem1  33581  heiborlem8  33588  heiborlem10  33590  heibor  33591  opidonOLD  33622  riscer  33758  crngohomfo  33776  keridl  33802  ispridl2  33808  ispridlc  33840  ac6s6  33951  dral1-o  34008  ax12indalem  34049  ax12inda2ALT  34050  lsatcveq0  34138  eqlkr3  34207  atlatmstc  34425  atlrelat1  34427  hlrelat2  34508  intnatN  34512  cvrexchlem  34524  cvratlem  34526  cvrat2  34534  atltcvr  34540  cvrat3  34547  cvrat4  34548  ps-1  34582  ps-2  34583  lplnnle2at  34646  lvolnle3at  34687  2llnma3r  34893  cdlemblem  34898  pmapjoin  34957  elpcliN  34998  lhpmcvr4N  35131  4atexlemnclw  35175  trlnidatb  35283  cdlemc4  35300  cdlemd3  35306  cdleme3g  35340  cdleme7d  35352  cdleme11c  35367  cdleme11dN  35368  cdleme21b  35433  cdleme21c  35434  cdleme21i  35442  cdleme22b  35448  cdleme35fnpq  35556  cdlemf1  35668  trlord  35676  cdlemg6c  35727  dihglblem6  36448  dochlkr  36493  dochkrshp  36494  dihjat1lem  36536  dochexmidlem5  36572  dochexmidlem8  36575  fphpdo  37200  pellexlem5  37216  pellexlem6  37217  jm2.26lem3  37387  unxpwdom3  37484  ov2ssiunov2  37811  frege124d  37872  ordpss  38475  19.41rg  38586  stoweidlem34  40014  ralralimp  41058  zm1nn  41079  elfz2z  41088  smonoord  41105  iccpartlt  41124  iccelpart  41133  icceuelpartlem  41135  fargshiftf1  41141  pfxccatin12lem1  41188  reuccatpfxs1lem  41198  goldbachthlem2  41223  odz2prm2pw  41240  fmtnoprmfac1lem  41241  fmtnofac2lem  41245  prmdvdsfmtnof1  41264  sfprmdvdsmersenne  41285  lighneallem2  41288  lighneallem4  41292  gbegt5  41414  gbowge7  41416  bgoldbtbndlem4  41461  bgoldbtbnd  41462  tgoldbach  41470  tgoldbachOLD  41477  sprsymrelf1lem  41506  zrtermorngc  41766  zrtermoringc  41835  lcosslsp  41992  lindslinindsimp1  42011  snlindsntor  42025  m1modmmod  42081  setrec1lem4  42202  aacllem  42312
  Copyright terms: Public domain W3C validator