Theorem syld 45

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 25899 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  147  pm2.61d  163  sylibd  222  sylbid  223  sylibrd  242  sylbird  243  syland  488  a2andOLD  826  ax12v  1944  alrimdd  1968  axc112  2030  nfeqf2  2145  sbequi  2214  2eu1  2392  axext3  2443  trel3  4518  poss  4775  sess2  4821  wefrc  4846  wereu2  4849  funun  5642  ssimaex  5952  f1imass  6189  soisoi  6243  isores3  6250  isofrlem  6255  isoselem  6256  weniso  6269  oninton  6653  orduniorsuc  6683  limuni3  6705  tfindsg  6713  limom  6733  f1o2ndf1  6930  soxp  6935  extmptsuppeq  6965  wfrlem12  7072  smoel  7104  smogt  7111  tfrlem9  7128  tz7.49  7187  seqomlem1  7192  odi  7305  omass  7306  omeulem2  7309  oeordsuc  7320  oeeulem  7327  ertr  7403  swoord2  7418  ecopovtrn  7491  domtriord  7743  onomeneq  7787  unxpdomlem2  7802  isinf  7810  pssnn  7815  findcard3  7839  frfi  7841  unblem3  7850  dffi3  7970  en3lplem1  8144  inf3lem3  8160  inf3lem5  8162  noinfep  8190  cantnfle  8201  cantnfp1lem3  8210  rankxpsuc  8378  tcrank  8380  ficardom  8420  carduni  8440  infxpenlem  8469  dfac8alem  8485  ac10ct  8490  ween  8491  alephdom  8537  alephle  8544  iscard3  8549  alephfp  8564  cdainf  8647  pwsdompw  8659  infdif  8664  cfslbn  8722  cofsmo  8724  cfsmolem  8725  cfcof  8729  fin1a2s  8869  domtriomlem  8897  ac6num  8934  zorn2lem3  8953  axdclem2  8975  imadomg  8987  iundom2g  8990  ficard  9015  fpwwe2lem8  9087  fpwwe2  9093  gchaclem  9128  tskr1om2  9218  inar1  9225  tskord  9230  tskuni  9233  grudomon  9267  grur1a  9269  grur1  9270  addnidpi  9351  ltexnq  9425  genpnnp  9455  addclprlem2  9467  mulclprlem  9469  psslinpr  9481  ltaddpr2  9485  ltexprlem6  9491  ltexprlem7  9492  addcanpr  9496  mulgt0sr  9554  map2psrpr  9559  supsrlem  9560  axrrecex  9612  letr  9752  dedekind  9822  recex  10271  lemul12b  10489  mulgt1  10491  fimaxre2  10579  lbreu  10583  nnrecgt0  10674  nnunb  10893  bndndx  10896  zeo  11049  uzind  11055  fzind  11061  fnn0ind  11062  suprfinzcl  11078  suprzcl2  11282  zmax  11289  rpnnen1lem5  11322  xrletr  11483  qbtwnre  11520  qsqueeze  11522  qextltlem  11523  xralrple  11526  xlesubadd  11577  supxrunb1  11633  icoshft  11782  fzen  11844  elfz1b  11892  elfz0fzfz0  11924  elfzmlbmOLD  11930  elfzmlbp  11931  fzo1fzo0n0  11987  elfzo0z  11988  fzofzim  11992  elfzodifsumelfzo  12010  ssfzoulel  12035  modadd1  12165  modmul1  12174  uzrdgfni  12203  fsuppmapnn0fiub0  12236  fsuppmapnn0ub  12238  fsuppmapnn0fz  12239  seqcl2  12262  seqfveq2  12266  seqshft2  12270  monoord  12274  seqsplit  12277  seqf1olem1  12283  seqf1olem2  12284  seqid2  12290  seqhomo  12291  expnbnd  12432  faclbnd4lem4  12512  seqcoll  12659  elss2prb  12675  swrdsbslen  12840  swrdspsleq  12841  swrdswrdlem  12851  swrdswrd  12852  reuccats1lem  12872  swrdccatin12lem2a  12877  swrdccatin12lem2b  12878  swrdccatin12lem3  12882  swrdccat3a  12886  swrdccat3blem  12887  repswswrd  12923  swrd2lsw  13075  sqeqd  13277  sqrmo  13363  cau3lem  13465  icodiamlt  13545  limsupbnd2  13594  limsupbnd2OLD  13595  lo1bdd2  13636  climuni  13664  rlimcn2  13702  mulcn2  13707  o1of2  13724  rlimo1  13728  lo1le  13763  isercolllem1  13776  iseralt  13799  cvgrat  13987  fprodss  14050  rpnnen2  14326  ruclem3  14333  sqrt2irr  14349  dvds2lem  14363  dvdslelem  14397  divalglem8  14428  bitsinv1lem  14463  sadcaddlem  14479  smu01lem  14507  smueqlem  14512  bezoutlem4OLD  14554  bezoutlem4  14557  algcvga  14586  lcmf  14654  lcmfunsnlem1  14658  lcmfunsnlem2lem1  14659  lcmfunsnlem2lem2  14660  lcmfdvdsb  14664  isprm3  14681  prmdvdsfz  14697  isprm5  14699  coprmgcdb  14702  coprm  14705  coprmdvds2  14708  rpexp12i  14722  ncoprmlnprm  14725  coprmprod  14726  phibndlem  14766  dfphi2  14770  eulerthlem2  14778  odzdvds  14788  odzdvdsOLD  14794  iserodd  14833  pclem  14836  pcpremul  14841  pcqcl  14854  pcdvdsb  14866  pcprmpw2  14879  pcaddlem  14881  pcmptcl  14884  pcfac  14892  prmpwdvds  14896  unbenlem  14900  prmreclem1  14908  4sqlem17OLD  14953  4sqlem17  14959  vdwmc2  14977  vdwlem9  14987  vdwlem10  14988  vdwlem13  14991  vdwnnlem3  14995  ramcl  15035  prmgaplem7  15075  mreiincl  15550  initoid  15948  termoid  15949  initoeu1  15954  initoeu2lem1  15957  termoeu1  15961  pospo  16267  dirge  16531  gsmsymgrfixlem1  17116  oddvdsnn0  17241  oddvds  17244  odcl2  17264  gexdvds  17283  sylow1lem1  17298  sylow2alem2  17318  sylow2a  17319  efgi2  17423  efgsrel  17432  efgs1b  17434  cyggex2  17579  telgsums  17671  pgpfac1lem2  17756  pgpfac1lem3a  17757  pgpfac1lem3  17758  pgpfac1lem5  17760  lssssr  18224  cply1mul  18935  gsummoncoe1  18946  gzrngunitlem  19080  znunit  19182  frgpcyg  19192  lsmcss  19303  obselocv  19339  obslbs  19341  scmataddcl  19589  scmatsubcl  19590  cpmatacl  19788  cpmatinvcl  19789  cpmatmcllem  19790  m2cpminvid2lem  19826  mp2pm2mplem4  19881  pm2mp  19897  chfacfisf  19926  chfacfisfcpmat  19927  chfacfscmul0  19930  chfacfpmmul0  19934  cayhamlem4  19960  ordtrest2lem  20267  leordtval2  20276  lecldbas  20283  cncls  20338  cncnp  20344  cnpresti  20352  lmcnp  20368  cnt0  20410  isreg2  20441  cmpsublem  20462  cmpsub  20463  tgcmp  20464  bwth  20473  dfcon2  20482  1stcfb  20508  2ndcctbss  20518  1stcelcls  20524  islly2  20547  dislly  20560  reftr  20577  comppfsc  20595  kgencn2  20620  txcnp  20683  txindis  20697  txcmplem1  20704  txlm  20711  xkohaus  20716  cnmptcom  20741  kqfvima  20793  isr0  20800  fgss2  20937  fbasrn  20947  filuni  20948  ufilmax  20970  isufil2  20971  cfinufil  20991  fmfnfmlem1  21017  fmfnfmlem2  21018  fmfnfmlem4  21020  fmfnfm  21021  fmco  21024  flimopn  21038  hausflim  21044  flimrest  21046  fclsopn  21077  flimfnfcls  21091  alexsubALTlem2  21111  alexsubALTlem3  21112  alexsubALT  21114  ptcmplem2  21116  cnextcn  21130  symgtgp  21164  qustgplem  21183  tsmsres  21206  tsmsxplem1  21215  isucn2  21342  imasdsf1olem  21436  bldisj  21461  blssps  21487  blss  21488  metcnp3  21603  ngptgp  21692  nrginvrcn  21742  nmoleub  21784  nmoleubOLD  21800  xrsmopn  21878  icccmplem3  21890  reconnlem2  21893  rectbntr0  21898  rescncf  21977  iocopnst  22016  iccpnfcnv  22020  lebnumii  22045  nmoleub2lem  22176  nmhmcn  22182  fgcfil  22289  iscfil3  22291  iscau2  22295  iscau3  22296  iscau4  22297  iscmet3lem2  22310  cfilres  22314  caussi  22315  equivcfil  22317  equivcau  22318  ivthlem2  22451  ivthlem3  22452  ovoliunlem2  22504  ovoliunnul  22508  ovolicc2lem3  22520  ioombl1lem4  22562  dyadmax  22604  dyadmbl  22606  volsup2  22611  itg2le  22745  itg2const2  22747  itg2seq  22748  itgsplitioo  22843  dvnres  22933  rolle  22990  c1lip1  22997  dvivthlem1  23008  lhop1  23014  dvcnvrelem1  23017  dvfsumrlim  23031  ply1divmo  23134  ig1peu  23170  ig1peuOLD  23171  plypf1  23214  coeaddlem  23251  fta1  23309  quotcan  23310  aalioulem4  23339  ulmcaulem  23397  ulmcn  23402  pilem2  23455  pilem2OLD  23456  sincosq1lem  23500  sinq12gt0  23510  sinq12ge0  23511  sineq0  23524  tanord1  23534  lognegb  23587  logrec  23748  dcubic  23820  xrlimcnp  23942  o1cxp  23948  ftalem2  24046  ftalem3  24047  fsumdvdscom  24162  chtub  24188  vmasum  24192  bcmono  24253  bposlem3  24262  bposlem7  24266  lgsdir  24306  lgsqrlem2  24318  lgsdchr  24324  lgsquadlem2  24331  2sqlem6  24345  dchrisumlem3  24377  pntrsumbnd2  24453  pntpbnd1  24472  pntibnd  24479  pntlem3  24495  pntleml  24497  brbtwn2  24983  colinearalg  24988  axcontlem10  25051  redwlk  25384  usgra2adedgspthlem2  25388  fargshiftf1  25413  constr3trllem2  25427  4cycl4dv  25443  usg2wlkeq  25484  wwlknred  25499  wwlknextbi  25501  wwlkm1edg  25511  clwlkswlks  25534  clwlkisclwwlklem2fv2  25559  clwlkisclwwlklem2a  25561  clwlkisclwwlklem1  25563  clwwlkf  25570  clwwlkext2edg  25578  wwlksubclwwlk  25580  clwwisshclwwlem1  25581  usg2wotspth  25660  vdusgra0nedg  25684  usgravd0nedg  25694  usgravd00  25695  eupath2  25756  frgraregorufrg  25848  numclwwlkovf2ex  25862  numclwlk1lem2foa  25867  numclwlk1lem2fo  25871  ex-natded5.3-2  25906  isgrpo  25972  opidonOLD  26098  vacn  26378  ubthlem2  26561  htthlem  26618  normgt0  26828  shmodsi  27090  spansneleq  27271  h1datomi  27282  pjjsi  27401  nmcexi  27727  pjnormssi  27869  stm1add3i  27948  golem2  27973  cvnsym  27991  dmdmd  28001  mdslmd1lem1  28026  mdslmd1i  28030  mdexchi  28036  atcveq0  28049  superpos  28055  hatomistici  28063  atoml2i  28084  atcvat2i  28088  chirredlem1  28091  atcvat3i  28097  mdsymlem3  28106  mdsymlem5  28108  cdj3lem2b  28138  cdj3i  28142  supssd  28338  infssd  28339  2sqmod  28457  resspos  28468  resstos  28469  submarchi  28551  tpr2rico  28766  ordtrest2NEWlem  28776  xrge0iifcnv  28787  omssubadd  29176  omssubaddOLD  29180  eulerpartlemb  29249  ballotlemfc0  29373  ballotlemfcc  29374  subfacp1lem6  29956  iccllyscon  30021  cvmfolem  30050  cvmliftlem7  30062  cvmliftlem10  30065  ghomf1olem  30360  fundmpss  30455  dfon2lem3  30479  dfon2lem6  30482  axext4dist  30495  trpredtr  30519  trpredmintr  30520  dftrpred3g  30522  trpredrec  30527  frmin  30528  soseq  30540  frrlem5e  30570  frrlem11  30574  sltval2  30591  sltres  30599  nosepon  30604  nodenselem4  30621  nodenselem8  30625  nobndlem6  30634  dfrdg4  30766  5segofs  30821  cgrextend  30823  segconeu  30826  btwncomim  30828  btwnswapid  30832  btwnintr  30834  btwnexch3  30835  btwndiff  30842  ifscgr  30859  cgrxfr  30870  btwnxfr  30871  lineext  30891  brofs2  30892  linecgr  30896  lineid  30898  idinside  30899  endofsegid  30900  btwnconn1lem13  30914  btwnconn3  30918  finminlem  31022  nn0prpwlem  31026  cldbnd  31030  clsint2  31033  fnessref  31061  neibastop3  31066  fgmin  31074  onsuct0  31149  limsucncmpi  31153  bj-exalimi  31269  wl-aetr  31907  wl-ax12v2  31953  fin2so  31976  tan2h  31981  poimirlem2  31986  poimirlem9  31993  poimirlem17  32001  poimirlem18  32002  poimirlem21  32005  poimirlem23  32007  poimirlem26  32010  poimirlem29  32013  poimirlem30  32014  poimirlem31  32015  poimir  32017  heicant  32019  mblfinlem2  32022  mblfinlem3  32023  itg2addnclem  32037  itg2addnclem2  32038  itg2gt0cn  32041  ftc1anclem5  32065  ftc1anclem6  32066  filbcmb  32111  nninfnub  32124  mettrifi  32130  geomcau  32132  istotbnd3  32147  sstotbnd2  32150  ismtybndlem  32182  heibor1lem  32185  heiborlem1  32187  heiborlem8  32194  heiborlem10  32196  heibor  32197  riscer  32271  crngohomfo  32283  keridl  32309  ispridl2  32315  ispridlc  32347  ac6s6  32459  dral1-o  32518  ax12indalem  32560  ax12inda2ALT  32561  lsatcveq0  32642  eqlkr3  32711  atlatmstc  32929  atlrelat1  32931  hlrelat2  33012  intnatN  33016  cvrexchlem  33028  cvratlem  33030  cvrat2  33038  atltcvr  33044  cvrat3  33051  cvrat4  33052  ps-1  33086  ps-2  33087  lplnnle2at  33150  lvolnle3at  33191  2llnma3r  33397  cdlemblem  33402  pmapjoin  33461  elpcliN  33502  lhpmcvr4N  33635  4atexlemnclw  33679  trlnidatb  33787  cdlemc4  33804  cdlemd3  33810  cdleme3g  33844  cdleme7d  33856  cdleme11c  33871  cdleme11dN  33872  cdleme21b  33937  cdleme21c  33938  cdleme21i  33946  cdleme22b  33952  cdleme35fnpq  34060  cdlemf1  34172  trlord  34180  cdlemg6c  34231  dihglblem6  34952  dochlkr  34997  dochkrshp  34998  dihjat1lem  35040  dochexmidlem5  35076  dochexmidlem8  35079  fphpdo  35704  pellexlem5  35721  pellexlem6  35722  jm2.26lem3  35900  dfac21  35968  unxpwdom3  35997  ov2ssiunov2  36336  frege124d  36397  ordpss  36847  19.41rg  36960  stoweidlem34  37932  smonoord  38755  iccpartlt  38775  iccelpart  38784  icceuelpartlem  38786  gbegt5  38899  gboge7  38901  nnsum3primesle9  38926  evengpop3  38930  evengpoap3  38931  bgoldbtbndlem4  38940  bgoldbtbnd  38941  tgoldbach  38948  pfxccatin12lem1  39003  reuccatpfxs1lem  39013  ralralimp  39026  f1cofveqaeq  39054  fundmge2nop  39067  zm1nn  39090  ltsubnn0  39092  elfz2z  39096  edgupgr  39272  upgredg  39275  usgruspgrb  39315  subupgr  39408  uhgrspan1  39424  uvtxupgrres  39530  usgredgsscusgredg  39569  upgrewlkle2  39672  red1wlk  39716  1wlkdlem2  39725  upgrwlkdvdelem  39767  pthdlem1  39791  pthdlem2  39793  umgr2adedgspth  39896  usgedgimp  39987  usgvincvad  39988  usgedgimpALT  39990  usgvincvadALT  39991  zrtermorngc  40275  zrtermoringc  40344  ztprmneprm  40400  lcosslsp  40503  lindslinindsimp1  40522  lindslinindsimp2lem5  40527  snlindsntor  40536  m1modmmod  40596  flnn0div2ge  40612  aacllem  40812