Theorem syld 45

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 25788 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  1910  alrimdd  1935  axc112  1997  nfeqf2  2102  sbequi  2175  2eu1  2354  axext3  2405  trel3  4464  poss  4714  sess2  4760  wefrc  4785  wereu2  4788  funun  5581  ssimaex  5885  f1imass  6119  soisoi  6173  isores3  6180  isofrlem  6185  isoselem  6186  weniso  6199  oninton  6580  orduniorsuc  6610  limuni3  6632  tfindsg  6640  limom  6660  f1o2ndf1  6854  soxp  6859  extmptsuppeq  6889  wfrlem12  6997  smoel  7029  smogt  7036  tfrlem9  7053  tz7.49  7112  seqomlem1  7117  odi  7230  omass  7231  omeulem2  7234  oeordsuc  7245  oeeulem  7252  ertr  7328  swoord2  7343  ecopovtrn  7416  domtriord  7666  onomeneq  7710  unxpdomlem2  7725  isinf  7733  pssnn  7738  findcard3  7762  frfi  7764  unblem3  7773  dffi3  7893  en3lplem1  8067  inf3lem3  8083  inf3lem5  8085  noinfep  8112  cantnfle  8123  cantnfp1lem3  8132  rankxpsuc  8300  tcrank  8302  ficardom  8342  carduni  8362  infxpenlem  8391  dfac8alem  8406  ac10ct  8411  ween  8412  alephdom  8458  alephle  8465  iscard3  8470  alephfp  8485  cdainf  8568  pwsdompw  8580  infdif  8585  cfslbn  8643  cofsmo  8645  cfsmolem  8646  cfcof  8650  fin1a2s  8790  domtriomlem  8818  ac6num  8855  zorn2lem3  8874  axdclem2  8896  imadomg  8908  iundom2g  8911  ficard  8936  fpwwe2lem8  9008  fpwwe2  9014  gchaclem  9049  tskr1om2  9139  inar1  9146  tskord  9151  tskuni  9154  grudomon  9188  grur1a  9190  grur1  9191  addnidpi  9272  ltexnq  9346  genpnnp  9376  addclprlem2  9388  mulclprlem  9390  psslinpr  9402  ltaddpr2  9406  ltexprlem6  9412  ltexprlem7  9413  addcanpr  9417  mulgt0sr  9475  map2psrpr  9480  supsrlem  9481  axrrecex  9533  letr  9673  dedekind  9743  recex  10190  lemul12b  10408  mulgt1  10410  fimaxre2  10498  lbreu  10502  nnrecgt0  10593  nnunb  10811  bndndx  10814  zeo  10967  uzind  10973  fzind  10979  fnn0ind  10980  suprfinzcl  10996  suprzcl2  11200  zmax  11207  rpnnen1lem5  11240  xrletr  11401  qbtwnre  11438  qsqueeze  11440  qextltlem  11441  xralrple  11444  xlesubadd  11495  supxrunb1  11551  icoshft  11700  fzen  11762  elfz1b  11810  elfz0fzfz0  11841  elfzmlbmOLD  11847  elfzmlbp  11848  fzo1fzo0n0  11903  elfzo0z  11904  fzofzim  11908  elfzodifsumelfzo  11925  ssfzoulel  11950  modadd1  12079  modmul1  12088  uzrdgfni  12117  fsuppmapnn0fiub0  12150  fsuppmapnn0ub  12152  fsuppmapnn0fz  12153  seqcl2  12176  seqfveq2  12180  seqshft2  12184  monoord  12188  seqsplit  12191  seqf1olem1  12197  seqf1olem2  12198  seqid2  12204  seqhomo  12205  expnbnd  12346  faclbnd4lem4  12426  seqcoll  12570  elss2prb  12586  swrdsbslen  12745  swrdspsleq  12746  swrdswrdlem  12756  swrdswrd  12757  reuccats1lem  12777  swrdccatin12lem2a  12782  swrdccatin12lem2b  12783  swrdccatin12lem3  12787  swrdccat3a  12791  swrdccat3blem  12792  repswswrd  12828  swrd2lsw  12966  sqeqd  13168  sqrmo  13254  cau3lem  13356  limsupbnd2  13484  limsupbnd2OLD  13485  lo1bdd2  13526  climuni  13554  rlimcn2  13592  mulcn2  13597  o1of2  13614  rlimo1  13618  lo1le  13653  isercolllem1  13666  iseralt  13689  cvgrat  13877  fprodss  13940  rpnnen2  14216  ruclem3  14223  sqrt2irr  14239  dvds2lem  14253  dvdslelem  14287  divalglem8  14318  bitsinv1lem  14353  sadcaddlem  14369  smu01lem  14397  smueqlem  14402  bezoutlem4OLD  14444  bezoutlem4  14447  algcvga  14476  lcmf  14544  lcmfunsnlem1  14548  lcmfunsnlem2lem1  14549  lcmfunsnlem2lem2  14550  lcmfdvdsb  14554  isprm3  14571  prmdvdsfz  14587  isprm5  14589  coprmgcdb  14592  coprm  14595  coprmdvds2  14598  rpexp12i  14612  ncoprmlnprm  14615  coprmprod  14616  phibndlem  14656  dfphi2  14660  eulerthlem2  14668  odzdvds  14678  odzdvdsOLD  14684  iserodd  14723  pclem  14726  pcpremul  14731  pcqcl  14744  pcdvdsb  14756  pcprmpw2  14769  pcaddlem  14771  pcmptcl  14774  pcfac  14782  prmpwdvds  14786  unbenlem  14790  prmreclem1  14798  4sqlem17OLD  14843  4sqlem17  14849  vdwmc2  14867  vdwlem9  14877  vdwlem10  14878  vdwlem13  14881  vdwnnlem3  14885  ramcl  14925  prmgaplem7  14965  mreiincl  15440  initoid  15838  termoid  15839  initoeu1  15844  initoeu2lem1  15847  termoeu1  15851  pospo  16157  dirge  16421  gsmsymgrfixlem1  17006  oddvdsnn0  17131  oddvds  17134  odcl2  17154  gexdvds  17173  sylow1lem1  17188  sylow2alem2  17208  sylow2a  17209  efgi2  17313  efgsrel  17322  efgs1b  17324  cyggex2  17469  telgsums  17561  pgpfac1lem2  17646  pgpfac1lem3a  17647  pgpfac1lem3  17648  pgpfac1lem5  17650  lssssr  18114  cply1mul  18825  gsummoncoe1  18836  gzrngunitlem  18970  znunit  19071  frgpcyg  19081  lsmcss  19192  obselocv  19228  obslbs  19230  scmataddcl  19478  scmatsubcl  19479  cpmatacl  19677  cpmatinvcl  19678  cpmatmcllem  19679  m2cpminvid2lem  19715  mp2pm2mplem4  19770  pm2mp  19786  chfacfisf  19815  chfacfisfcpmat  19816  chfacfscmul0  19819  chfacfpmmul0  19823  cayhamlem4  19849  ordtrest2lem  20156  leordtval2  20165  lecldbas  20172  cncls  20227  cncnp  20233  cnpresti  20241  lmcnp  20257  cnt0  20299  isreg2  20330  cmpsublem  20351  cmpsub  20352  tgcmp  20353  bwth  20362  dfcon2  20371  1stcfb  20397  2ndcctbss  20407  1stcelcls  20413  islly2  20436  dislly  20449  reftr  20466  comppfsc  20484  kgencn2  20509  txcnp  20572  txindis  20586  txcmplem1  20593  txlm  20600  xkohaus  20605  cnmptcom  20630  kqfvima  20682  isr0  20689  fgss2  20826  fbasrn  20836  filuni  20837  ufilmax  20859  isufil2  20860  cfinufil  20880  fmfnfmlem1  20906  fmfnfmlem2  20907  fmfnfmlem4  20909  fmfnfm  20910  fmco  20913  flimopn  20927  hausflim  20933  flimrest  20935  fclsopn  20966  flimfnfcls  20980  alexsubALTlem2  21000  alexsubALTlem3  21001  alexsubALT  21003  ptcmplem2  21005  cnextcn  21019  symgtgp  21053  qustgplem  21072  tsmsres  21095  tsmsxplem1  21104  isucn2  21231  imasdsf1olem  21325  bldisj  21350  blssps  21376  blss  21377  metcnp3  21492  ngptgp  21581  nrginvrcn  21631  nmoleub  21673  nmoleubOLD  21689  xrsmopn  21767  icccmplem3  21779  reconnlem2  21782  rectbntr0  21787  rescncf  21866  iocopnst  21905  iccpnfcnv  21909  lebnumii  21934  nmoleub2lem  22065  nmhmcn  22071  fgcfil  22178  iscfil3  22180  iscau2  22184  iscau3  22185  iscau4  22186  iscmet3lem2  22199  cfilres  22203  caussi  22204  equivcfil  22206  equivcau  22207  ivthlem2  22340  ivthlem3  22341  ovoliunlem2  22393  ovoliunnul  22397  ovolicc2lem3  22409  ioombl1lem4  22451  dyadmax  22493  dyadmbl  22495  volsup2  22500  itg2le  22634  itg2const2  22636  itg2seq  22637  itgsplitioo  22732  dvnres  22822  rolle  22879  c1lip1  22886  dvivthlem1  22897  lhop1  22903  dvcnvrelem1  22906  dvfsumrlim  22920  ply1divmo  23023  ig1peu  23059  ig1peuOLD  23060  plypf1  23103  coeaddlem  23140  fta1  23198  quotcan  23199  aalioulem4  23228  ulmcaulem  23286  ulmcn  23291  pilem2  23344  pilem2OLD  23345  sincosq1lem  23389  sinq12gt0  23399  sinq12ge0  23400  sineq0  23413  tanord1  23423  lognegb  23476  logrec  23637  dcubic  23709  xrlimcnp  23831  o1cxp  23837  ftalem2  23935  ftalem3  23936  fsumdvdscom  24051  chtub  24077  vmasum  24081  bcmono  24142  bposlem3  24151  bposlem7  24155  lgsdir  24195  lgsqrlem2  24207  lgsdchr  24213  lgsquadlem2  24220  2sqlem6  24234  dchrisumlem3  24266  pntrsumbnd2  24342  pntpbnd1  24361  pntibnd  24368  pntlem3  24384  pntleml  24386  brbtwn2  24872  colinearalg  24877  axcontlem10  24940  redwlk  25273  usgra2adedgspthlem2  25277  fargshiftf1  25302  constr3trllem2  25316  4cycl4dv  25332  usg2wlkeq  25373  wwlknred  25388  wwlknextbi  25390  wwlkm1edg  25400  clwlkswlks  25423  clwlkisclwwlklem2fv2  25448  clwlkisclwwlklem2a  25450  clwlkisclwwlklem1  25452  clwwlkf  25459  clwwlkext2edg  25467  wwlksubclwwlk  25469  clwwisshclwwlem1  25470  usg2wotspth  25549  vdusgra0nedg  25573  usgravd0nedg  25583  usgravd00  25584  eupath2  25645  frgraregorufrg  25737  numclwwlkovf2ex  25751  numclwlk1lem2foa  25756  numclwlk1lem2fo  25760  ex-natded5.3-2  25795  isgrpo  25861  opidonOLD  25987  vacn  26267  ubthlem2  26450  htthlem  26507  normgt0  26717  shmodsi  26979  spansneleq  27160  h1datomi  27171  pjjsi  27290  nmcexi  27616  pjnormssi  27758  stm1add3i  27837  golem2  27862  cvnsym  27880  dmdmd  27890  mdslmd1lem1  27915  mdslmd1i  27919  mdexchi  27925  atcveq0  27938  superpos  27944  hatomistici  27952  atoml2i  27973  atcvat2i  27977  chirredlem1  27980  atcvat3i  27986  mdsymlem3  27995  mdsymlem5  27997  cdj3lem2b  28027  cdj3i  28031  supssd  28231  infssd  28232  2sqmod  28355  resspos  28366  resstos  28367  submarchi  28449  tpr2rico  28665  ordtrest2NEWlem  28675  xrge0iifcnv  28686  omssubadd  29075  omssubaddOLD  29079  eulerpartlemb  29148  ballotlemfc0  29272  ballotlemfcc  29273  subfacp1lem6  29855  iccllyscon  29920  cvmfolem  29949  cvmliftlem7  29961  cvmliftlem10  29964  ghomf1olem  30259  fundmpss  30353  dfon2lem3  30377  dfon2lem6  30380  axext4dist  30393  trpredtr  30417  trpredmintr  30418  dftrpred3g  30420  trpredrec  30425  frmin  30426  soseq  30438  frrlem5e  30468  frrlem11  30472  sltval2  30489  sltres  30497  nodenselem4  30517  nodenselem8  30521  nobndlem6  30530  dfrdg4  30662  5segofs  30717  cgrextend  30719  segconeu  30722  btwncomim  30724  btwnswapid  30728  btwnintr  30730  btwnexch3  30731  btwndiff  30738  ifscgr  30755  cgrxfr  30766  btwnxfr  30767  lineext  30787  brofs2  30788  linecgr  30792  lineid  30794  idinside  30795  endofsegid  30796  btwnconn1lem13  30810  btwnconn3  30814  finminlem  30918  nn0prpwlem  30922  cldbnd  30926  clsint2  30929  fnessref  30957  neibastop3  30962  fgmin  30970  onsuct0  31045  limsucncmpi  31049  bj-exalimi  31164  wl-aetr  31770  wl-ax12v2  31816  fin2so  31839  tan2h  31844  poimirlem2  31849  poimirlem9  31856  poimirlem17  31864  poimirlem18  31865  poimirlem21  31868  poimirlem23  31870  poimirlem26  31873  poimirlem29  31876  poimirlem30  31877  poimirlem31  31878  poimir  31880  heicant  31882  mblfinlem2  31885  mblfinlem3  31886  itg2addnclem  31900  itg2addnclem2  31901  itg2gt0cn  31904  ftc1anclem5  31928  ftc1anclem6  31929  filbcmb  31974  nninfnub  31987  mettrifi  31993  geomcau  31995  istotbnd3  32010  sstotbnd2  32013  ismtybndlem  32045  heibor1lem  32048  heiborlem1  32050  heiborlem8  32057  heiborlem10  32059  heibor  32060  riscer  32134  crngohomfo  32146  keridl  32172  ispridl2  32178  ispridlc  32210  ac6s6  32322  dral1-o  32386  ax12indalem  32428  ax12inda2ALT  32429  lsatcveq0  32510  eqlkr3  32579  atlatmstc  32797  atlrelat1  32799  hlrelat2  32880  intnatN  32884  cvrexchlem  32896  cvratlem  32898  cvrat2  32906  atltcvr  32912  cvrat3  32919  cvrat4  32920  ps-1  32954  ps-2  32955  lplnnle2at  33018  lvolnle3at  33059  2llnma3r  33265  cdlemblem  33270  pmapjoin  33329  elpcliN  33370  lhpmcvr4N  33503  4atexlemnclw  33547  trlnidatb  33655  cdlemc4  33672  cdlemd3  33678  cdleme3g  33712  cdleme7d  33724  cdleme11c  33739  cdleme11dN  33740  cdleme21b  33805  cdleme21c  33806  cdleme21i  33814  cdleme22b  33820  cdleme35fnpq  33928  cdlemf1  34040  trlord  34048  cdlemg6c  34099  dihglblem6  34820  dochlkr  34865  dochkrshp  34866  dihjat1lem  34908  dochexmidlem5  34944  dochexmidlem8  34947  fphpdo  35572  icodiamlt  35577  pellexlem5  35590  pellexlem6  35591  jm2.26lem3  35769  dfac21  35837  unxpwdom3  35866  ov2ssiunov2  36205  frege124d  36266  ordpss  36717  19.41rg  36830  stoweidlem34  37778  smonoord  38531  iccpartlt  38551  iccelpart  38560  icceuelpartlem  38562  gbegt5  38675  gboge7  38677  nnsum3primesle9  38702  evengpop3  38706  evengpoap3  38707  bgoldbtbndlem4  38716  bgoldbtbnd  38717  tgoldbach  38724  pfxccatin12lem1  38777  reuccatpfxs1lem  38787  ralralimp  38798  fundmge2nop  38832  zm1nn  38846  ltsubnn0  38848  elfz2z  38852  edgupgr  38988  upgredg  38990  usgruspgrb  39024  subupgr  39096  uhgrspan1  39112  uvtxupgrres  39209  usgredgsscusgredg  39248  usgedgimp  39306  usgvincvad  39307  usgedgimpALT  39309  usgvincvadALT  39310  zrtermorngc  39594  zrtermoringc  39663  ztprmneprm  39721  lcosslsp  39824  lindslinindsimp1  39843  lindslinindsimp2lem5  39848  snlindsntor  39857  m1modmmod  39917  flnn0div2ge  39933  aacllem  40133