Theorem syld 47

Description: Syllogism deduction. Deduction associated with syl 17. See conventions 27258 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 25	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	1, 3	mpdd 43	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:  syldc  48  3syld  60  sylsyld  61  nsyld  154  pm2.61d  170  sylibd  229  sylbid  230  sylibrd  249  sylbird  250  syland  498  ax12v2  2049  ax12vOLD  2050  ax12vOLDOLD  2051  alrimdd  2083  axc16g  2134  axc16nf  2137  axc11rvOLD  2140  axc11r  2187  alrimddOLD  2195  nfeqf2  2297  sbequi  2375  2eu1  2553  axext3  2604  trel3  4760  poss  5037  sess2  5083  wefrc  5108  wereu2  5111  funun  5932  ssimaex  6263  f1cofveqaeq  6515  f1imass  6521  soisoi  6578  isores3  6585  isofrlem  6590  isoselem  6591  weniso  6604  abnexg  6964  oninton  7000  orduniorsuc  7030  limuni3  7052  tfindsg  7060  limom  7080  f1o2ndf1  7285  soxp  7290  extmptsuppeq  7319  smoel  7457  tfrlem9  7481  tz7.49  7540  seqomlem1  7545  odi  7659  omass  7660  omeulem2  7663  oeordsuc  7674  oeeulem  7681  ertr  7757  swoord2  7774  ecopovtrn  7850  domtriord  8106  onomeneq  8150  unxpdomlem2  8165  isinf  8173  pssnn  8178  findcard3  8203  frfi  8205  unblem3  8214  dffi3  8337  en3lplem1  8511  inf3lem5  8529  cantnfle  8568  cantnfp1lem3  8577  rankxpsuc  8745  tcrank  8747  ficardom  8787  carduni  8807  infxpenlem  8836  dfac8alem  8852  ac10ct  8857  ween  8858  alephdom  8904  alephle  8911  iscard3  8916  alephfp  8931  cdainf  9014  pwsdompw  9026  infdif  9031  cfslbn  9089  cofsmo  9091  cfcof  9096  fin1a2s  9236  domtriomlem  9264  ac6num  9301  zorn2lem3  9320  axdclem2  9342  imadomg  9356  iundom2g  9362  ficard  9387  fpwwe2lem8  9459  fpwwe2  9465  gchaclem  9500  tskr1om2  9590  inar1  9597  tskord  9602  tskuni  9605  grudomon  9639  grur1a  9641  grur1  9642  addnidpi  9723  ltexnq  9797  genpnnp  9827  addclprlem2  9839  mulclprlem  9841  psslinpr  9853  ltexprlem6  9863  ltexprlem7  9864  addcanpr  9868  mulgt0sr  9926  map2psrpr  9931  supsrlem  9932  axrrecex  9984  letr  10131  dedekind  10200  recex  10659  lemul12b  10880  mulgt1  10882  fimaxre2  10969  lbreu  10973  nnrecgt0  11058  nnunb  11288  bndndx  11291  zeo  11463  uzind  11469  fzind  11475  fnn0ind  11476  suprfinzcl  11492  suprzcl2  11778  zmax  11785  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  xrletr  11989  qbtwnre  12030  qsqueeze  12032  qextltlem  12033  xralrple  12036  xlesubadd  12093  supxrunb1  12149  icoshft  12294  zltaddlt1le  12324  fzen  12358  elfz0fzfz0  12444  elfzmlbp  12450  elfzo0z  12509  fzofzim  12514  fzo1fzo0n0  12518  elfzodifsumelfzo  12533  ssfzoulel  12562  modadd1  12707  modmul1  12723  uzrdgfni  12757  fsuppmapnn0fiub0  12793  fsuppmapnn0ub  12795  fsuppmapnn0fz  12796  seqcl2  12819  seqfveq2  12823  seqshft2  12827  monoord  12831  seqsplit  12834  seqf1olem1  12840  seqf1olem2  12841  seqid2  12847  seqhomo  12848  expnbnd  12993  faclbnd4lem4  13083  seqcoll  13248  hashle2pr  13259  elss2prb  13269  ccatalpha  13375  swrdsbslen  13448  swrdspsleq  13449  swrdswrdlem  13459  swrdswrd  13460  reuccats1lem  13479  swrdccatin12lem2a  13485  swrdccatin12lem2b  13486  swrdccatin12lem3  13490  swrdccat3a  13494  swrdccat3blem  13495  repswswrd  13531  cshf1  13556  swrd2lsw  13695  sqeqd  13906  sqrmo  13992  cau3lem  14094  icodiamlt  14174  limsupbnd2  14214  lo1bdd2  14255  climuni  14283  rlimcn2  14321  mulcn2  14326  o1of2  14343  rlimo1  14347  lo1le  14382  isercolllem1  14395  iseralt  14415  cvgrat  14615  fprodss  14678  znnenlem  14940  rpnnen2lem12  14954  ruclem3  14962  sqrt2irr  14979  dvds2lem  14994  dvdslelem  15031  dvdsabseq  15035  divalglem8  15123  bitsinv1lem  15163  sadcaddlem  15179  smu01lem  15207  smueqlem  15212  bezoutlem4  15259  dfgcd2  15263  algcvga  15292  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  lcmfdvdsb  15356  coprmgcdb  15362  coprmdvds2  15368  coprmprod  15375  isprm3  15396  prmdvdsfz  15417  isprm5  15419  coprm  15423  rpexp12i  15434  phibndlem  15475  dfphi2  15479  eulerthlem2  15487  odzdvds  15500  iserodd  15540  pclem  15543  pcpremul  15548  pcqcl  15561  pcdvdsb  15573  pcprmpw2  15586  difsqpwdvds  15591  pcaddlem  15592  pcmptcl  15595  pcfac  15603  prmpwdvds  15608  unbenlem  15612  prmreclem1  15620  4sqlem17  15665  vdwmc2  15683  vdwlem9  15693  vdwlem10  15694  vdwlem13  15697  vdwnnlem3  15701  ramcl  15733  prmgaplem7  15761  mreiincl  16256  initoid  16655  termoid  16656  initoeu2lem1  16664  pospo  16973  dirge  17237  gsmsymgrfixlem1  17847  oddvdsnn0  17963  oddvds  17966  odcl2  17982  gexdvds  17999  sylow1lem1  18013  sylow2alem2  18033  sylow2a  18034  efgi2  18138  efgsrel  18147  efgs1b  18149  cyggex2  18298  telgsums  18390  pgpfac1lem2  18474  pgpfac1lem3a  18475  pgpfac1lem3  18476  pgpfac1lem5  18478  lmodfopnelem2  18900  lssssr  18953  cply1mul  19664  gsummoncoe1  19674  gzrngunitlem  19811  znunit  19912  frgpcyg  19922  lsmcss  20036  obselocv  20072  obslbs  20074  cpmatacl  20521  cpmatinvcl  20522  cpmatmcllem  20523  m2cpminvid2lem  20559  mp2pm2mplem4  20614  pm2mp  20630  chfacfisf  20659  chfacfisfcpmat  20660  chfacfscmul0  20663  chfacfpmmul0  20667  cayhamlem4  20693  ordtrest2lem  21007  leordtval2  21016  lecldbas  21023  cncls  21078  cncnp  21084  cnpresti  21092  lmcnp  21108  cnt0  21150  isreg2  21181  cmpsublem  21202  cmpsub  21203  tgcmp  21204  bwth  21213  dfconn2  21222  1stcfb  21248  1stcelcls  21264  islly2  21287  dislly  21300  reftr  21317  comppfsc  21335  kgencn2  21360  txcnp  21423  txindis  21437  txcmplem1  21444  txlm  21451  xkohaus  21456  cnmptcom  21481  kqfvima  21533  isr0  21540  fgss2  21678  fbasrn  21688  filuni  21689  ufilmax  21711  isufil2  21712  cfinufil  21732  fmfnfmlem1  21758  fmfnfmlem2  21759  fmfnfmlem4  21761  fmfnfm  21762  fmco  21765  flimopn  21779  hausflim  21785  flimrest  21787  fclsopn  21818  flimfnfcls  21832  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALT  21855  ptcmplem2  21857  cnextcn  21871  symgtgp  21905  qustgplem  21924  tsmsres  21947  tsmsxplem1  21956  isucn2  22083  imasdsf1olem  22178  bldisj  22203  blssps  22229  blss  22230  metcnp3  22345  ngptgp  22440  nrginvrcn  22496  nmoleub  22535  xrsmopn  22615  icccmplem3  22627  reconnlem2  22630  rectbntr0  22635  rescncf  22700  iocopnst  22739  iccpnfcnv  22743  lebnumii  22765  nmoleub2lem  22914  nmhmcn  22920  iscfil3  23071  iscau2  23075  iscau3  23076  iscau4  23077  iscmet3lem2  23090  cfilres  23094  caussi  23095  equivcfil  23097  equivcau  23098  ivthlem2  23221  ivthlem3  23222  ovoliunlem2  23271  ovoliunnul  23275  ovolicc2lem3  23287  ioombl1lem4  23329  dyadmax  23366  dyadmbl  23368  volsup2  23373  itg2le  23506  itg2const2  23508  itg2seq  23509  itgsplitioo  23604  dvnres  23694  rolle  23753  c1lip1  23760  dvivthlem1  23771  lhop1  23777  dvcnvrelem1  23780  dvfsumrlim  23794  ply1divmo  23895  ig1peu  23931  plypf1  23968  coeaddlem  24005  fta1  24063  quotcan  24064  aalioulem4  24090  ulmcaulem  24148  ulmcn  24153  pilem2  24206  sincosq1lem  24249  sinq12gt0  24259  sinq12ge0  24260  tanord1  24283  lognegb  24336  logrec  24501  dcubic  24573  xrlimcnp  24695  o1cxp  24701  ftalem2  24800  ftalem3  24801  fsumdvdscom  24911  chtub  24937  vmasum  24941  bcmono  25002  bposlem3  25011  bposlem7  25015  lgsdir  25057  lgsqrlem2  25072  lgsqrmodndvds  25078  lgsdchr  25080  gausslemma2dlem6  25097  gausslemma2d  25099  lgsquadlem2  25106  2lgslem3a1  25125  2lgslem3b1  25126  2lgslem3c1  25127  2lgslem3d1  25128  2sqlem6  25148  dchrisumlem3  25180  pntrsumbnd2  25256  pntpbnd1  25275  pntibnd  25282  pntlem3  25298  pntleml  25300  brbtwn2  25785  colinearalg  25790  axcontlem10  25853  edgupgr  26029  edglnl  26038  usgruspgrb  26076  subupgr  26179  uhgrspan1  26195  usgredgsscusgredg  26355  fusgrn0degnn0  26395  upgrewlkle2  26502  uspgr2wlkeq  26542  redwlk  26569  wlkdlem2  26580  upgrwlkdvdelem  26632  pthdlem1  26662  pthdlem2  26664  crctcshwlkn0lem3  26704  wlkiswwlks1  26753  wwlksm1edg  26767  wwlksnred  26787  wwlksnextbi  26789  umgr2adedgspth  26844  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a  26899  clwwlksf  26915  clwwlksext2edg  26923  wwlksubclwwlks  26925  clwwisshclwwslemlem  26926  eupth2lems  27098  frgrwopreglem4a  27174  frgrregorufrg  27190  numclwwlkovf2exlem2  27212  numclwlk1lem2fo  27228  ex-natded5.3-2  27265  isgrpo  27351  vacn  27549  ubthlem2  27727  htthlem  27774  normgt0  27984  shmodsi  28248  spansneleq  28429  h1datomi  28440  nmcexi  28885  pjnormssi  29027  stm1add3i  29106  golem2  29131  cvnsym  29149  dmdmd  29159  mdslmd1lem1  29184  mdslmd1i  29188  mdexchi  29194  atcveq0  29207  superpos  29213  hatomistici  29221  atoml2i  29242  atcvat2i  29246  chirredlem1  29249  atcvat3i  29255  mdsymlem3  29264  mdsymlem5  29266  cdj3lem2b  29296  cdj3i  29300  supssd  29487  infssd  29488  2sqmod  29648  resspos  29659  resstos  29660  submarchi  29740  tpr2rico  29958  ordtrest2NEWlem  29968  xrge0iifcnv  29979  omssubadd  30362  eulerpartlemb  30430  ballotlemfc0  30554  ballotlemfcc  30555  ftc2re  30676  subfacp1lem6  31167  iccllysconn  31232  cvmfolem  31261  cvmliftlem7  31273  cvmliftlem10  31276  fundmpss  31664  dfon2lem3  31690  dfon2lem6  31693  axext4dist  31706  trpredtr  31730  trpredmintr  31731  dftrpred3g  31733  trpredrec  31738  frmin  31739  soseq  31751  frrlem5e  31788  sltres  31815  nosepon  31818  nolesgn2o  31824  nodenselem8  31841  nosupbnd1lem1  31854  dfrdg4  32058  5segofs  32113  cgrextend  32115  segconeu  32118  btwncomim  32120  btwnswapid  32124  btwnintr  32126  btwnexch3  32127  btwndiff  32134  ifscgr  32151  cgrxfr  32162  btwnxfr  32163  lineext  32183  brofs2  32184  linecgr  32188  lineid  32190  idinside  32191  endofsegid  32192  btwnconn1lem13  32206  btwnconn3  32210  finminlem  32312  nn0prpwlem  32317  cldbnd  32321  clsint2  32324  fnessref  32352  neibastop3  32357  fgmin  32365  onsuct0  32440  limsucncmpi  32444  bj-axc14  32839  bj-restn0  33043  bj-0int  33055  wl-19.2reqv  33310  wl-aetr  33317  fin2so  33396  tan2h  33401  lindsenlbs  33404  poimirlem2  33411  poimirlem9  33418  poimirlem17  33426  poimirlem18  33427  poimirlem21  33430  poimirlem23  33432  poimirlem26  33435  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimir  33442  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  itg2addnclem  33461  itg2addnclem2  33462  itg2gt0cn  33465  ftc1anclem5  33489  ftc1anclem6  33490  filbcmb  33535  nninfnub  33547  mettrifi  33553  geomcau  33555  istotbnd3  33570  sstotbnd2  33573  ismtybndlem  33605  heibor1lem  33608  heiborlem1  33610  heiborlem8  33617  heiborlem10  33619  heibor  33620  opidonOLD  33651  riscer  33787  crngohomfo  33805  keridl  33831  ispridl2  33837  ispridlc  33869  ac6s6  33980  dral1-o  34189  ax12indalem  34230  ax12inda2ALT  34231  lsatcveq0  34319  eqlkr3  34388  atlatmstc  34606  atlrelat1  34608  hlrelat2  34689  intnatN  34693  cvrexchlem  34705  cvratlem  34707  cvrat2  34715  atltcvr  34721  cvrat3  34728  cvrat4  34729  ps-1  34763  ps-2  34764  lplnnle2at  34827  lvolnle3at  34868  2llnma3r  35074  cdlemblem  35079  pmapjoin  35138  elpcliN  35179  lhpmcvr4N  35312  4atexlemnclw  35356  trlnidatb  35464  cdlemc4  35481  cdlemd3  35487  cdleme3g  35521  cdleme7d  35533  cdleme11c  35548  cdleme11dN  35549  cdleme21b  35614  cdleme21c  35615  cdleme21i  35623  cdleme22b  35629  cdleme35fnpq  35737  cdlemf1  35849  trlord  35857  cdlemg6c  35908  dihglblem6  36629  dochlkr  36674  dochkrshp  36675  dihjat1lem  36717  dochexmidlem5  36753  dochexmidlem8  36756  fphpdo  37381  pellexlem5  37397  pellexlem6  37398  jm2.26lem3  37568  unxpwdom3  37665  ov2ssiunov2  37992  frege124d  38053  ordpss  38655  19.41rg  38766  stoweidlem34  40251  ralralimp  41295  zm1nn  41316  elfz2z  41325  smonoord  41341  iccpartlt  41360  iccelpart  41369  icceuelpartlem  41371  fargshiftf1  41377  pfxccatin12lem1  41423  reuccatpfxs1lem  41433  goldbachthlem2  41458  odz2prm2pw  41475  fmtnoprmfac1lem  41476  fmtnofac2lem  41480  prmdvdsfmtnof1  41499  sfprmdvdsmersenne  41520  lighneallem2  41523  lighneallem4  41527  gbegt5  41649  gbowge7  41651  bgoldbtbndlem4  41696  bgoldbtbnd  41697  tgoldbach  41705  tgoldbachOLD  41712  sprsymrelf1lem  41741  zrtermorngc  42001  zrtermoringc  42070  lcosslsp  42227  lindslinindsimp1  42246  snlindsntor  42260  m1modmmod  42316  setrec1lem4  42437  aacllem  42547