Theorem syld 45

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 25687 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	|- ( ph -> ( ps -> ch ) )
syld.2	|- ( ph -> ( ch -> th ) )

Assertion

Ref	Expression
syld	|- ( ph -> ( ps -> th ) )

Proof of Theorem syld

Step	Hyp	Ref	Expression
1		syld.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syld.2	. . 3 |- ( ph -> ( ch -> th ) )
3	2	a1d 26	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	1, 3	mpdd 41	1 |- ( ph -> ( ps -> th ) )

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  145  pm2.61d  161  sylibd  217  sylbid  218  sylibrd  237  sylbird  238  syland  483  a2andOLD  819  ax12v  1908  alrimdd  1933  axc112  1995  nfeqf2  2097  sbequi  2170  2eu1  2354  axext3  2409  trel3  4528  poss  4777  sess2  4823  wefrc  4848  wereu2  4851  funun  5643  ssimaex  5946  f1imass  6180  soisoi  6234  isores3  6241  isofrlem  6246  isoselem  6247  weniso  6260  oninton  6641  orduniorsuc  6671  limuni3  6693  tfindsg  6701  limom  6721  f1o2ndf1  6915  soxp  6920  extmptsuppeq  6950  wfrlem12  7055  smoel  7087  smogt  7094  tfrlem9  7111  tz7.49  7170  seqomlem1  7175  odi  7288  omass  7289  omeulem2  7292  oeordsuc  7303  oeeulem  7310  ertr  7386  swoord2  7401  ecopovtrn  7474  domtriord  7724  onomeneq  7768  unxpdomlem2  7783  isinf  7791  pssnn  7796  findcard3  7820  frfi  7822  unblem3  7831  dffi3  7951  en3lplem1  8119  inf3lem3  8135  inf3lem5  8137  noinfep  8164  cantnfle  8175  cantnfp1lem3  8184  rankxpsuc  8352  tcrank  8354  ficardom  8394  carduni  8414  infxpenlem  8443  dfac8alem  8458  ac10ct  8463  ween  8464  alephdom  8510  alephle  8517  iscard3  8522  alephfp  8537  cdainf  8620  pwsdompw  8632  infdif  8637  cfslbn  8695  cofsmo  8697  cfsmolem  8698  cfcof  8702  fin1a2s  8842  domtriomlem  8870  ac6num  8907  zorn2lem3  8926  axdclem2  8948  imadomg  8960  iundom2g  8963  ficard  8988  fpwwe2lem8  9061  fpwwe2  9067  gchaclem  9102  tskr1om2  9192  inar1  9199  tskord  9204  tskuni  9207  grudomon  9241  grur1a  9243  grur1  9244  addnidpi  9325  ltexnq  9399  genpnnp  9429  addclprlem2  9441  mulclprlem  9443  psslinpr  9455  ltaddpr2  9459  ltexprlem6  9465  ltexprlem7  9466  addcanpr  9470  mulgt0sr  9528  map2psrpr  9533  supsrlem  9534  axrrecex  9586  letr  9726  dedekind  9796  recex  10243  lemul12b  10461  mulgt1  10463  fimaxre2  10552  lbreu  10556  nnrecgt0  10647  nnunb  10865  bndndx  10868  zeo  11021  uzind  11027  fzind  11033  fnn0ind  11034  suprfinzcl  11050  suprzcl2  11254  zmax  11261  rpnnen1lem5  11294  xrletr  11455  qbtwnre  11492  qsqueeze  11494  qextltlem  11495  xralrple  11498  xlesubadd  11549  supxrunb1  11605  icoshft  11752  fzen  11814  elfz1b  11862  elfz0fzfz0  11893  elfzmlbmOLD  11899  elfzmlbp  11900  fzo1fzo0n0  11955  elfzo0z  11956  fzofzim  11960  elfzodifsumelfzo  11977  ssfzoulel  12002  modadd1  12131  modmul1  12140  uzrdgfni  12169  fsuppmapnn0fiub0  12202  fsuppmapnn0ub  12204  fsuppmapnn0fz  12205  seqcl2  12228  seqfveq2  12232  seqshft2  12236  monoord  12240  seqsplit  12243  seqf1olem1  12249  seqf1olem2  12250  seqid2  12256  seqhomo  12257  expnbnd  12398  faclbnd4lem4  12478  seqcoll  12621  swrdsbslen  12789  swrdspsleq  12790  swrdswrdlem  12800  swrdswrd  12801  reuccats1lem  12821  swrdccatin12lem2a  12826  swrdccatin12lem2b  12827  swrdccatin12lem3  12831  swrdccat3a  12835  swrdccat3blem  12836  repswswrd  12872  swrd2lsw  13006  sqeqd  13208  sqrmo  13294  cau3lem  13396  limsupbnd2  13524  limsupbnd2OLD  13525  lo1bdd2  13566  climuni  13594  rlimcn2  13632  mulcn2  13637  o1of2  13654  rlimo1  13658  lo1le  13693  isercolllem1  13706  iseralt  13729  cvgrat  13917  fprodss  13980  rpnnen2  14256  ruclem3  14263  sqrt2irr  14279  dvds2lem  14293  dvdslelem  14327  divalglem8  14356  bitsinv1lem  14389  sadcaddlem  14405  smu01lem  14433  smueqlem  14438  bezoutlem4  14480  algcvga  14509  lcmf  14568  lcmfunsnlem1  14572  lcmfunsnlem2lem1  14573  lcmfunsnlem2lem2  14574  lcmfdvdsb  14578  isprm3  14595  prmdvdsfz  14611  isprm5  14613  coprmgcdb  14616  coprm  14619  coprmdvds2  14622  rpexp12i  14636  ncoprmlnprm  14639  coprmprod  14640  phibndlem  14678  dfphi2  14682  eulerthlem2  14690  odzdvds  14700  iserodd  14739  pclem  14742  pcpremul  14747  pcqcl  14760  pcdvdsb  14772  pcprmpw2  14785  pcaddlem  14787  pcmptcl  14790  pcfac  14798  prmpwdvds  14802  unbenlem  14806  prmreclem1  14814  4sqlem17OLD  14859  4sqlem17  14865  vdwmc2  14883  vdwlem9  14893  vdwlem10  14894  vdwlem13  14897  vdwnnlem3  14901  ramcl  14941  prmgaplem7  14981  mreiincl  15444  initoid  15842  termoid  15843  initoeu1  15848  initoeu2lem1  15851  termoeu1  15855  pospo  16161  dirge  16425  gsmsymgrfixlem1  17010  oddvdsnn0  17126  oddvds  17129  odcl2  17145  gexdvds  17162  sylow1lem1  17176  sylow2alem2  17196  sylow2a  17197  efgi2  17301  efgsrel  17310  efgs1b  17312  cyggex2  17457  telgsums  17549  pgpfac1lem2  17634  pgpfac1lem3a  17635  pgpfac1lem3  17636  pgpfac1lem5  17638  lssssr  18102  cply1mul  18813  gsummoncoe1  18824  gzrngunitlem  18958  znunit  19056  frgpcyg  19066  lsmcss  19177  obselocv  19213  obslbs  19215  scmataddcl  19463  scmatsubcl  19464  cpmatacl  19662  cpmatinvcl  19663  cpmatmcllem  19664  m2cpminvid2lem  19700  mp2pm2mplem4  19755  pm2mp  19771  chfacfisf  19800  chfacfisfcpmat  19801  chfacfscmul0  19804  chfacfpmmul0  19808  cayhamlem4  19834  ordtrest2lem  20141  leordtval2  20150  lecldbas  20157  cncls  20212  cncnp  20218  cnpresti  20226  lmcnp  20242  cnt0  20284  isreg2  20315  cmpsublem  20336  cmpsub  20337  tgcmp  20338  bwth  20347  dfcon2  20356  1stcfb  20382  2ndcctbss  20392  1stcelcls  20398  islly2  20421  dislly  20434  reftr  20451  comppfsc  20469  kgencn2  20494  txcnp  20557  txindis  20571  txcmplem1  20578  txlm  20585  xkohaus  20590  cnmptcom  20615  kqfvima  20667  isr0  20674  fgss2  20811  fbasrn  20821  filuni  20822  ufilmax  20844  isufil2  20845  cfinufil  20865  fmfnfmlem1  20891  fmfnfmlem2  20892  fmfnfmlem4  20894  fmfnfm  20895  fmco  20898  flimopn  20912  hausflim  20918  flimrest  20920  fclsopn  20951  flimfnfcls  20965  alexsubALTlem2  20985  alexsubALTlem3  20986  alexsubALT  20988  ptcmplem2  20990  cnextcn  21004  symgtgp  21038  qustgplem  21057  tsmsres  21080  tsmsxplem1  21089  isucn2  21216  imasdsf1olem  21310  bldisj  21335  blssps  21361  blss  21362  metcnp3  21477  ngptgp  21566  nrginvrcn  21616  nmoleub  21654  xrsmopn  21732  icccmplem3  21744  reconnlem2  21747  rectbntr0  21752  rescncf  21816  iocopnst  21855  iccpnfcnv  21859  lebnumii  21881  nmoleub2lem  22012  nmhmcn  22018  fgcfil  22125  iscfil3  22127  iscau2  22131  iscau3  22132  iscau4  22133  iscmet3lem2  22146  cfilres  22150  caussi  22151  equivcfil  22153  equivcau  22154  ivthlem2  22275  ivthlem3  22276  ovoliunlem2  22325  ovoliunnul  22329  ovolicc2lem3  22341  ioombl1lem4  22382  dyadmax  22424  dyadmbl  22426  volsup2  22431  itg2le  22565  itg2const2  22567  itg2seq  22568  itgsplitioo  22663  dvnres  22753  rolle  22810  c1lip1  22817  dvivthlem1  22828  lhop1  22834  dvcnvrelem1  22837  dvfsumrlim  22851  ply1divmo  22952  ig1peu  22988  plypf1  23025  coeaddlem  23062  fta1  23120  quotcan  23121  aalioulem4  23147  ulmcaulem  23205  ulmcn  23210  pilem2  23263  pilem2OLD  23264  sincosq1lem  23308  sinq12gt0  23318  sinq12ge0  23319  sineq0  23332  tanord1  23342  lognegb  23395  logrec  23556  dcubic  23628  xrlimcnp  23750  o1cxp  23756  ftalem2  23854  ftalem3  23855  fsumdvdscom  23968  chtub  23994  vmasum  23998  bcmono  24059  bposlem3  24068  bposlem7  24072  lgsdir  24112  lgsqrlem2  24124  lgsdchr  24130  lgsquadlem2  24137  2sqlem6  24151  dchrisumlem3  24183  pntrsumbnd2  24259  pntpbnd1  24278  pntibnd  24285  pntlem3  24301  pntleml  24303  brbtwn2  24772  colinearalg  24777  axcontlem10  24840  redwlk  25172  usgra2adedgspthlem2  25176  fargshiftf1  25201  constr3trllem2  25215  4cycl4dv  25231  usg2wlkeq  25272  wwlknred  25287  wwlknextbi  25289  wwlkm1edg  25299  clwlkswlks  25322  clwlkisclwwlklem2fv2  25347  clwlkisclwwlklem2a  25349  clwlkisclwwlklem1  25351  clwwlkf  25358  clwwlkext2edg  25366  wwlksubclwwlk  25368  clwwisshclwwlem1  25369  usg2wotspth  25448  vdusgra0nedg  25472  usgravd0nedg  25482  usgravd00  25483  eupath2  25544  frgraregorufrg  25636  numclwwlkovf2ex  25650  numclwlk1lem2foa  25655  numclwlk1lem2fo  25659  ex-natded5.3-2  25694  isgrpo  25760  opidonOLD  25886  vacn  26166  ubthlem2  26349  htthlem  26396  normgt0  26606  shmodsi  26868  spansneleq  27049  h1datomi  27060  pjjsi  27179  nmcexi  27505  pjnormssi  27647  stm1add3i  27726  golem2  27751  cvnsym  27769  dmdmd  27779  mdslmd1lem1  27804  mdslmd1i  27808  mdexchi  27814  atcveq0  27827  superpos  27833  hatomistici  27841  atoml2i  27862  atcvat2i  27866  chirredlem1  27869  atcvat3i  27875  mdsymlem3  27884  mdsymlem5  27886  cdj3lem2b  27916  cdj3i  27920  supssd  28121  2sqmod  28238  resspos  28249  resstos  28250  submarchi  28332  tpr2rico  28548  ordtrest2NEWlem  28558  xrge0iifcnv  28569  omssubadd  28952  eulerpartlemb  29018  ballotlemfc0  29142  ballotlemfcc  29143  subfacp1lem6  29687  iccllyscon  29752  cvmfolem  29781  cvmliftlem7  29793  cvmliftlem10  29796  ghomf1olem  30091  fundmpss  30185  dfon2lem3  30209  dfon2lem6  30212  axext4dist  30225  trpredtr  30249  trpredmintr  30250  dftrpred3g  30252  trpredrec  30257  frmin  30258  soseq  30270  frrlem5e  30300  frrlem11  30304  sltval2  30321  sltres  30329  nodenselem4  30349  nodenselem8  30353  nobndlem6  30362  dfrdg4  30494  5segofs  30549  cgrextend  30551  segconeu  30554  btwncomim  30556  btwnswapid  30560  btwnintr  30562  btwnexch3  30563  btwndiff  30570  ifscgr  30587  cgrxfr  30598  btwnxfr  30599  lineext  30619  brofs2  30620  linecgr  30624  lineid  30626  idinside  30627  endofsegid  30628  btwnconn1lem13  30642  btwnconn3  30646  finminlem  30750  nn0prpwlem  30754  cldbnd  30758  clsint2  30761  fnessref  30789  neibastop3  30794  fgmin  30802  onsuct0  30877  limsucncmpi  30881  bj-exalimi  30995  wl-aetr  31561  wl-ax12v2  31603  fin2so  31626  tan2h  31631  poimirlem2  31636  poimirlem9  31643  poimirlem17  31651  poimirlem18  31652  poimirlem21  31655  poimirlem23  31657  poimirlem26  31660  poimirlem29  31663  poimirlem30  31664  poimirlem31  31665  poimir  31667  heicant  31669  mblfinlem2  31672  mblfinlem3  31673  itg2addnclem  31687  itg2addnclem2  31688  itg2gt0cn  31691  ftc1anclem5  31715  ftc1anclem6  31716  filbcmb  31761  nninfnub  31774  mettrifi  31780  geomcau  31782  istotbnd3  31797  sstotbnd2  31800  ismtybndlem  31832  heibor1lem  31835  heiborlem1  31837  heiborlem8  31844  heiborlem10  31846  heibor  31847  riscer  31921  crngohomfo  31933  keridl  31959  ispridl2  31965  ispridlc  31997  ac6s6  32109  dral1-o  32173  ax12indalem  32215  ax12inda2ALT  32216  lsatcveq0  32297  eqlkr3  32366  atlatmstc  32584  atlrelat1  32586  hlrelat2  32667  intnatN  32671  cvrexchlem  32683  cvratlem  32685  cvrat2  32693  atltcvr  32699  cvrat3  32706  cvrat4  32707  ps-1  32741  ps-2  32742  lplnnle2at  32805  lvolnle3at  32846  2llnma3r  33052  cdlemblem  33057  pmapjoin  33116  elpcliN  33157  lhpmcvr4N  33290  4atexlemnclw  33334  trlnidatb  33442  cdlemc4  33459  cdlemd3  33465  cdleme3g  33499  cdleme7d  33511  cdleme11c  33526  cdleme11dN  33527  cdleme21b  33592  cdleme21c  33593  cdleme21i  33601  cdleme22b  33607  cdleme35fnpq  33715  cdlemf1  33827  trlord  33835  cdlemg6c  33886  dihglblem6  34607  dochlkr  34652  dochkrshp  34653  dihjat1lem  34695  dochexmidlem5  34731  dochexmidlem8  34734  fphpdo  35359  icodiamlt  35364  pellexlem5  35377  pellexlem6  35378  jm2.26lem3  35552  dfac21  35620  unxpwdom3  35649  ov2ssiunov2  35921  frege124d  35982  ordpss  36431  19.41rg  36544  stoweidlem34  37454  smonoord  38098  iccpartlt  38118  iccelpart  38127  icceuelpartlem  38129  gbegt5  38242  gboge7  38244  nnsum3primesle9  38269  evengpop3  38273  evengpoap3  38274  bgoldbtbndlem4  38283  bgoldbtbnd  38284  tgoldbach  38291  pfxccatin12lem1  38344  reuccatpfxs1lem  38354  ralralimp  38362  zm1nn  38388  ltsubnn0  38390  elfz2z  38394  usgedgimp  38463  usgvincvad  38464  usgedgimpALT  38466  usgvincvadALT  38467  zrtermorngc  38751  zrtermoringc  38820  ztprmneprm  38878  lcosslsp  38981  lindslinindsimp1  39000  lindslinindsimp2lem5  39005  snlindsntor  39014  m1modmmod  39075  flnn0div2ge  39091  aacllem  39291