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

Theorem syld 45
Description: Syllogism deduction. Deduction associated with syl 17. See conventions 26412 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 41 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:  3syld  57  sylsyld  58  nsyld  152  pm2.61d  168  sylibd  227  sylbid  228  sylibrd  247  sylbird  248  syland  496  ax12v2  2033  ax12vOLD  2034  ax12vOLDOLD  2035  alrimdd  2067  axc16g  2116  axc16nf  2119  axc11rvOLD  2122  axc11r  2169  alrimddOLD  2177  nfeqf2  2280  sbequi  2358  2eu1  2536  axext3  2587  trel3  4678  poss  4947  sess2  4993  wefrc  5018  wereu2  5021  funun  5828  ssimaex  6154  f1imass  6396  soisoi  6452  isores3  6459  isofrlem  6464  isoselem  6465  weniso  6478  oninton  6865  orduniorsuc  6895  limuni3  6917  tfindsg  6925  limom  6945  f1o2ndf1  7145  soxp  7150  extmptsuppeq  7179  wfrlem12  7286  smoel  7317  smogt  7324  tfrlem9  7341  tz7.49  7400  seqomlem1  7405  odi  7519  omass  7520  omeulem2  7523  oeordsuc  7534  oeeulem  7541  ertr  7617  swoord2  7634  ecopovtrn  7710  domtriord  7964  onomeneq  8008  unxpdomlem2  8023  isinf  8031  pssnn  8036  findcard3  8061  frfi  8063  unblem3  8072  dffi3  8193  en3lplem1  8367  inf3lem3  8383  inf3lem5  8385  noinfep  8413  cantnfle  8424  cantnfp1lem3  8433  rankxpsuc  8601  tcrank  8603  ficardom  8643  carduni  8663  infxpenlem  8692  dfac8alem  8708  ac10ct  8713  ween  8714  alephdom  8760  alephle  8767  iscard3  8772  alephfp  8787  cdainf  8870  pwsdompw  8882  infdif  8887  cfslbn  8945  cofsmo  8947  cfsmolem  8948  cfcof  8952  fin1a2s  9092  domtriomlem  9120  ac6num  9157  zorn2lem3  9176  axdclem2  9198  imadomg  9210  iundom2g  9214  ficard  9239  fpwwe2lem8  9311  fpwwe2  9317  gchaclem  9352  tskr1om2  9442  inar1  9449  tskord  9454  tskuni  9457  grudomon  9491  grur1a  9493  grur1  9494  addnidpi  9575  ltexnq  9649  genpnnp  9679  addclprlem2  9691  mulclprlem  9693  psslinpr  9705  ltaddpr2  9709  ltexprlem6  9715  ltexprlem7  9716  addcanpr  9720  mulgt0sr  9778  map2psrpr  9783  supsrlem  9784  axrrecex  9836  letr  9978  dedekind  10047  recex  10504  lemul12b  10725  mulgt1  10727  fimaxre2  10814  lbreu  10818  nnrecgt0  10901  nnunb  11131  bndndx  11134  zeo  11291  uzind  11297  fzind  11303  fnn0ind  11304  suprfinzcl  11320  suprzcl2  11606  zmax  11613  rpnnen1lem5  11646  rpnnen1lem5OLD  11652  xrletr  11820  qbtwnre  11859  qsqueeze  11861  qextltlem  11862  xralrple  11865  xlesubadd  11918  supxrunb1  11973  icoshft  12117  zltaddlt1le  12147  fzen  12180  elfz1b  12230  elfz0fzfz0  12264  elfzmlbp  12270  elfzo0z  12328  fzofzim  12333  fzo1fzo0n0  12337  elfzodifsumelfzo  12352  ssfzoulel  12379  modadd1  12520  modmul1  12536  uzrdgfni  12570  fsuppmapnn0fiub0  12606  fsuppmapnn0ub  12608  fsuppmapnn0fz  12609  seqcl2  12632  seqfveq2  12636  seqshft2  12640  monoord  12644  seqsplit  12647  seqf1olem1  12653  seqf1olem2  12654  seqid2  12660  seqhomo  12661  expnbnd  12806  faclbnd4lem4  12896  seqcoll  13053  elss2prb  13069  ccatalpha  13170  swrdsbslen  13242  swrdspsleq  13243  swrdswrdlem  13253  swrdswrd  13254  reuccats1lem  13273  swrdccatin12lem2a  13278  swrdccatin12lem2b  13279  swrdccatin12lem3  13283  swrdccat3a  13287  swrdccat3blem  13288  repswswrd  13324  cshf1  13349  swrd2lsw  13485  sqeqd  13696  sqrmo  13782  cau3lem  13884  icodiamlt  13964  limsupbnd2  14004  lo1bdd2  14045  climuni  14073  rlimcn2  14111  mulcn2  14116  o1of2  14133  rlimo1  14137  lo1le  14172  isercolllem1  14185  iseralt  14205  cvgrat  14396  fprodss  14459  znnenlem  14721  rpnnen2lem12  14735  ruclem3  14743  sqrt2irr  14759  dvds2lem  14774  dvdslelem  14811  dvdsabseq  14815  divalglem8  14903  bitsinv1lem  14943  sadcaddlem  14959  smu01lem  14987  smueqlem  14992  bezoutlem4  15039  dfgcd2  15043  algcvga  15072  lcmf  15126  lcmfunsnlem1  15130  lcmfunsnlem2lem1  15131  lcmfunsnlem2lem2  15132  lcmfdvdsb  15136  coprmgcdb  15142  coprmdvds2  15148  coprmprod  15155  isprm3  15176  prmdvdsfz  15197  isprm5  15199  coprm  15203  rpexp12i  15214  ncoprmlnprm  15216  phibndlem  15255  dfphi2  15259  eulerthlem2  15267  odzdvds  15280  iserodd  15320  pclem  15323  pcpremul  15328  pcqcl  15341  pcdvdsb  15353  pcprmpw2  15366  difsqpwdvds  15371  pcaddlem  15372  pcmptcl  15375  pcfac  15383  prmpwdvds  15388  unbenlem  15392  prmreclem1  15400  4sqlem17  15445  vdwmc2  15463  vdwlem9  15473  vdwlem10  15474  vdwlem13  15477  vdwnnlem3  15481  ramcl  15513  prmgaplem7  15541  mreiincl  16021  initoid  16420  termoid  16421  initoeu1  16426  initoeu2lem1  16429  termoeu1  16433  pospo  16738  dirge  17002  dfgrp3lem  17278  gsmsymgrfixlem1  17612  oddvdsnn0  17728  oddvds  17731  odcl2  17747  gexdvds  17764  sylow1lem1  17778  sylow2alem2  17798  sylow2a  17799  efgi2  17903  efgsrel  17912  efgs1b  17914  cyggex2  18063  telgsums  18155  pgpfac1lem2  18239  pgpfac1lem3a  18240  pgpfac1lem3  18241  pgpfac1lem5  18243  lmodfopnelem2  18665  lssssr  18716  cply1mul  19427  gsummoncoe1  19437  gzrngunitlem  19572  znunit  19672  frgpcyg  19682  lsmcss  19793  obselocv  19829  obslbs  19831  scmataddcl  20079  scmatsubcl  20080  cpmatacl  20278  cpmatinvcl  20279  cpmatmcllem  20280  m2cpminvid2lem  20316  mp2pm2mplem4  20371  pm2mp  20387  chfacfisf  20416  chfacfisfcpmat  20417  chfacfscmul0  20420  chfacfpmmul0  20424  cayhamlem4  20450  ordtrest2lem  20755  leordtval2  20764  lecldbas  20771  cncls  20826  cncnp  20832  cnpresti  20840  lmcnp  20856  cnt0  20898  isreg2  20929  cmpsublem  20950  cmpsub  20951  tgcmp  20952  bwth  20961  dfcon2  20970  1stcfb  20996  2ndcctbss  21006  1stcelcls  21012  islly2  21035  dislly  21048  reftr  21065  comppfsc  21083  kgencn2  21108  txcnp  21171  txindis  21185  txcmplem1  21192  txlm  21199  xkohaus  21204  cnmptcom  21229  kqfvima  21281  isr0  21288  fgss2  21426  fbasrn  21436  filuni  21437  ufilmax  21459  isufil2  21460  cfinufil  21480  fmfnfmlem1  21506  fmfnfmlem2  21507  fmfnfmlem4  21509  fmfnfm  21510  fmco  21513  flimopn  21527  hausflim  21533  flimrest  21535  fclsopn  21566  flimfnfcls  21580  alexsubALTlem2  21600  alexsubALTlem3  21601  alexsubALT  21603  ptcmplem2  21605  cnextcn  21619  symgtgp  21653  qustgplem  21672  tsmsres  21695  tsmsxplem1  21704  isucn2  21831  imasdsf1olem  21925  bldisj  21950  blssps  21976  blss  21977  metcnp3  22092  ngptgp  22184  nrginvrcn  22235  nmoleub  22273  xrsmopn  22351  icccmplem3  22363  reconnlem2  22366  rectbntr0  22371  rescncf  22435  iocopnst  22474  iccpnfcnv  22478  lebnumii  22500  nmoleub2lem  22649  nmhmcn  22655  fgcfil  22791  iscfil3  22793  iscau2  22797  iscau3  22798  iscau4  22799  iscmet3lem2  22812  cfilres  22816  caussi  22817  equivcfil  22819  equivcau  22820  ivthlem2  22941  ivthlem3  22942  ovoliunlem2  22991  ovoliunnul  22995  ovolicc2lem3  23007  ioombl1lem4  23049  dyadmax  23085  dyadmbl  23087  volsup2  23092  itg2le  23225  itg2const2  23227  itg2seq  23228  itgsplitioo  23323  dvnres  23413  rolle  23470  c1lip1  23477  dvivthlem1  23488  lhop1  23494  dvcnvrelem1  23497  dvfsumrlim  23511  ply1divmo  23612  ig1peu  23648  plypf1  23685  coeaddlem  23722  fta1  23780  quotcan  23781  aalioulem4  23807  ulmcaulem  23865  ulmcn  23870  pilem2  23923  sincosq1lem  23966  sinq12gt0  23976  sinq12ge0  23977  tanord1  24000  lognegb  24053  logrec  24214  dcubic  24286  xrlimcnp  24408  o1cxp  24414  ftalem2  24513  ftalem3  24514  fsumdvdscom  24624  chtub  24650  vmasum  24654  bcmono  24715  bposlem3  24724  bposlem7  24728  lgsdir  24770  lgsqrlem2  24785  lgsqrmodndvds  24791  lgsdchr  24793  gausslemma2dlem6  24810  gausslemma2d  24812  lgsquadlem2  24819  2lgslem3a1  24838  2lgslem3b1  24839  2lgslem3c1  24840  2lgslem3d1  24841  2sqlem6  24861  dchrisumlem3  24893  pntrsumbnd2  24969  pntpbnd1  24988  pntibnd  24995  pntlem3  25011  pntleml  25013  brbtwn2  25499  colinearalg  25504  axcontlem10  25567  redwlk  25898  usgra2adedgspthlem2  25902  fargshiftf1  25927  constr3trllem2  25941  4cycl4dv  25957  usg2wlkeq  25998  wwlknred  26013  wwlknextbi  26015  wwlkm1edg  26025  clwlkswlks  26048  clwlkisclwwlklem2fv2  26073  clwlkisclwwlklem2a  26075  clwlkisclwwlklem1  26077  clwwlkf  26084  clwwlkext2edg  26092  wwlksubclwwlk  26094  clwwisshclwwlem1  26095  usg2wotspth  26173  vdusgra0nedg  26197  usgravd0nedg  26207  usgravd00  26208  eupath2  26269  frgraregorufrg  26361  numclwwlkovf2ex  26375  numclwlk1lem2foa  26380  numclwlk1lem2fo  26384  ex-natded5.3-2  26419  isgrpo  26497  vacn  26730  ubthlem2  26913  htthlem  26960  normgt0  27170  shmodsi  27434  spansneleq  27615  h1datomi  27626  pjjsi  27745  nmcexi  28071  pjnormssi  28213  stm1add3i  28292  golem2  28317  cvnsym  28335  dmdmd  28345  mdslmd1lem1  28370  mdslmd1i  28374  mdexchi  28380  atcveq0  28393  superpos  28399  hatomistici  28407  atoml2i  28428  atcvat2i  28432  chirredlem1  28435  atcvat3i  28441  mdsymlem3  28450  mdsymlem5  28452  cdj3lem2b  28482  cdj3i  28486  supssd  28672  infssd  28673  2sqmod  28781  resspos  28792  resstos  28793  submarchi  28873  tpr2rico  29088  ordtrest2NEWlem  29098  xrge0iifcnv  29109  omssubadd  29491  eulerpartlemb  29559  ballotlemfc0  29683  ballotlemfcc  29684  subfacp1lem6  30223  iccllyscon  30288  cvmfolem  30317  cvmliftlem7  30329  cvmliftlem10  30332  fundmpss  30712  dfon2lem3  30736  dfon2lem6  30739  axext4dist  30752  trpredtr  30776  trpredmintr  30777  dftrpred3g  30779  trpredrec  30784  frmin  30785  soseq  30797  frrlem5e  30834  frrlem11  30838  sltval2  30855  sltres  30863  nosepon  30868  nodenselem4  30885  nodenselem8  30889  nobndlem6  30898  dfrdg4  31030  5segofs  31085  cgrextend  31087  segconeu  31090  btwncomim  31092  btwnswapid  31096  btwnintr  31098  btwnexch3  31099  btwndiff  31106  ifscgr  31123  cgrxfr  31134  btwnxfr  31135  lineext  31155  brofs2  31156  linecgr  31160  lineid  31162  idinside  31163  endofsegid  31164  btwnconn1lem13  31178  btwnconn3  31182  finminlem  31284  nn0prpwlem  31289  cldbnd  31293  clsint2  31296  fnessref  31324  neibastop3  31329  fgmin  31337  onsuct0  31412  limsucncmpi  31416  bj-exalimi  31603  bj-restn0  32023  wl-19.2reqv  32288  wl-dveeq12  32289  wl-aetr  32295  fin2so  32365  tan2h  32370  lindsenlbs  32373  poimirlem2  32380  poimirlem9  32387  poimirlem17  32395  poimirlem18  32396  poimirlem21  32399  poimirlem23  32401  poimirlem26  32404  poimirlem29  32407  poimirlem30  32408  poimirlem31  32409  poimir  32411  heicant  32413  mblfinlem2  32416  mblfinlem3  32417  itg2addnclem  32430  itg2addnclem2  32431  itg2gt0cn  32434  ftc1anclem5  32458  ftc1anclem6  32459  filbcmb  32504  nninfnub  32516  mettrifi  32522  geomcau  32524  istotbnd3  32539  sstotbnd2  32542  ismtybndlem  32574  heibor1lem  32577  heiborlem1  32579  heiborlem8  32586  heiborlem10  32588  heibor  32589  opidonOLD  32620  riscer  32756  crngohomfo  32774  keridl  32800  ispridl2  32806  ispridlc  32838  ac6s6  32949  dral1-o  33006  ax12indalem  33047  ax12inda2ALT  33048  lsatcveq0  33136  eqlkr3  33205  atlatmstc  33423  atlrelat1  33425  hlrelat2  33506  intnatN  33510  cvrexchlem  33522  cvratlem  33524  cvrat2  33532  atltcvr  33538  cvrat3  33545  cvrat4  33546  ps-1  33580  ps-2  33581  lplnnle2at  33644  lvolnle3at  33685  2llnma3r  33891  cdlemblem  33896  pmapjoin  33955  elpcliN  33996  lhpmcvr4N  34129  4atexlemnclw  34173  trlnidatb  34281  cdlemc4  34298  cdlemd3  34304  cdleme3g  34338  cdleme7d  34350  cdleme11c  34365  cdleme11dN  34366  cdleme21b  34431  cdleme21c  34432  cdleme21i  34440  cdleme22b  34446  cdleme35fnpq  34554  cdlemf1  34666  trlord  34674  cdlemg6c  34725  dihglblem6  35446  dochlkr  35491  dochkrshp  35492  dihjat1lem  35534  dochexmidlem5  35570  dochexmidlem8  35573  fphpdo  36198  pellexlem5  36214  pellexlem6  36215  jm2.26lem3  36385  dfac21  36453  unxpwdom3  36482  ov2ssiunov2  36810  frege124d  36871  ordpss  37475  19.41rg  37586  stoweidlem34  38727  smonoord  39745  iccpartlt  39763  iccelpart  39772  icceuelpartlem  39774  goldbachthlem2  39797  odz2prm2pw  39814  fmtnoprmfac1lem  39815  fmtnofac2lem  39819  prmdvdsfmtnof1  39838  sfprmdvdsmersenne  39859  lighneallem2  39862  lighneallem4  39866  gbegt5  39984  gboge7  39986  nnsum3primesle9  40011  evengpop3  40015  evengpoap3  40016  bgoldbtbndlem4  40025  bgoldbtbnd  40026  tgoldbach  40033  tgoldbachOLD  40040  pfxccatin12lem1  40087  reuccatpfxs1lem  40097  ralralimp  40110  f1cofveqaeq  40135  fundmge2nop0  40148  zm1nn  40171  elfz2z  40175  edgupgr  40365  upgredg  40368  usgruspgrb  40409  subupgr  40509  uhgrspan1  40525  usgredgsscusgredg  40673  fusgrn0degnn0  40712  upgrewlkle2  40806  uspgr2wlkeq  40852  red1wlk  40879  1wlkdlem2  40890  upgrwlkdvdelem  40940  pthdlem1  40970  pthdlem2  40972  crctcsh1wlkn0lem3  41013  0enwwlksnge1  41058  1wlkiswwlks1  41062  wwlksm1edg  41076  wwlksnred  41096  wwlksnextbi  41098  umgr2adedgspth  41153  clwlkclwwlklem2fv2  41203  clwlkclwwlklem2a  41205  clwlkclwwlklem2  41207  clwwlksf  41220  clwwlksext2edg  41228  wwlksubclwwlks  41230  clwwisshclwwslemlem  41231  clwlksfclwwlk  41267  conngrv2edg  41360  eupth2lems  41404  frgrregorufrg  41503  av-numclwwlkovf2ex  41515  av-numclwlk1lem2foa  41519  av-numclwlk1lem2fo  41523  zrtermorngc  41791  zrtermoringc  41860  ztprmneprm  41916  lcosslsp  42019  lindslinindsimp1  42038  lindslinindsimp2lem5  42043  snlindsntor  42052  m1modmmod  42108  flnn0div2ge  42119  aacllem  42315
  Copyright terms: Public domain W3C validator