Theorem syld 42

Description: Syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

Notice that syld 42 has the same form as syl 16 with ph added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace ph with a hypothesis of the proof, allowing the hypothesis to be eliminated with id 20 and become an antecedent. The Deduction Theorem for propositional calculus, e.g. Theorem 3 in [Margaris] p. 56, tells us that this procedure is always possible.

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 23	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	1, 3	mpdd 38	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4

This theorem is referenced by:  3syld  53  sylsyld  54  nsyld  134  pm2.61d  152  sylibd  206  sylbid  207  sylibrd  226  sylbird  227  syland  468  alrimdd  1780  ax12olem3  1974  ax10lem3  1990  dvelimvOLD  1994  dral1OLD  2023  cbv1h  2031  sbied  2085  sbequi  2108  dral1-o  2204  ax11indalem  2247  ax11inda2ALT  2248  trel3  4270  poss  4465  sess2  4511  wefrc  4536  wereu2  4539  ordelord  4563  oninton  4739  orduniorsuc  4769  limuni3  4791  tfindsg  4799  limom  4819  funun  5454  ssimaex  5747  f1dmex  5930  f1imass  5969  soisoi  6007  isores3  6014  isofrlem  6019  isoselem  6020  weniso  6034  f1o2ndf1  6413  soxp  6418  riotasv3dOLD  6558  smoel  6581  smogt  6588  tfrlem9  6605  tz7.49  6661  seqomlem1  6666  abianfp  6675  odi  6781  omass  6782  omeulem2  6785  oeordsuc  6796  oeeulem  6803  ertr  6879  swoord2  6894  ecopovtrn  6966  domtriord  7212  2pwuninel  7221  onomeneq  7255  unxpdomlem2  7273  isinf  7281  pssnn  7286  findcard3  7309  frfi  7311  unblem3  7320  dffi3  7394  inf3lem3  7541  inf3lem5  7543  noinfep  7570  cantnfle  7582  cantnfp1lem3  7592  en3lplem1  7626  rankxpsuc  7762  tcrank  7764  ficardom  7804  carduni  7824  infxpenlem  7851  dfac8alem  7866  ac10ct  7871  ween  7872  alephdom  7918  alephle  7925  iscard3  7930  alephfp  7945  cdainf  8028  pwsdompw  8040  infdif  8045  cfslbn  8103  cofsmo  8105  cfsmolem  8106  cfcof  8110  fin1a2s  8250  domtriomlem  8278  ac6num  8315  zorn2lem3  8334  axdclem2  8356  imadomg  8368  iundom2g  8371  ficard  8396  fpwwe2lem8  8468  fpwwe2  8474  gchaclem  8501  tskr1om2  8599  inar1  8606  tskord  8611  tskuni  8614  grudomon  8648  grur1a  8650  grur1  8651  addnidpi  8734  ltexnq  8808  genpnnp  8838  addclprlem2  8850  mulclprlem  8852  psslinpr  8864  ltaddpr2  8868  ltexprlem6  8874  ltexprlem7  8875  addcanpr  8879  mulgt0sr  8936  map2psrpr  8941  supsrlem  8942  axrrecex  8994  letr  9123  recex  9610  lemul12b  9823  mulgt1  9825  ledivmulOLD  9840  fimaxre2  9912  lbreu  9914  nnrecgt0  9993  nnunb  10173  bndndx  10176  zeo  10311  uzind  10317  fzind  10324  fnn0ind  10325  lbzbi  10520  suprzcl2  10522  zmax  10527  rpnnen1lem5  10560  xrletr  10704  qbtwnre  10741  qsqueeze  10743  qextltlem  10744  xralrple  10747  xlesubadd  10798  supxrunb1  10854  icoshft  10975  fzen  11028  modadd1  11233  modmul1  11234  uzrdgfni  11253  seqcl2  11296  seqfveq2  11300  seqshft2  11304  monoord  11308  seqsplit  11311  seqf1olem1  11317  seqf1olem2  11318  seqid2  11324  seqhomo  11325  expnbnd  11463  faclbnd4lem4  11542  seqcoll  11667  sqeqd  11926  sqrmo  12012  cau3lem  12113  limsupbnd2  12232  lo1bdd2  12273  climuni  12301  rlimcn2  12339  mulcn2  12344  o1of2  12361  rlimo1  12365  lo1le  12400  isercolllem1  12413  iseralt  12433  isumrpcl  12578  cvgrat  12615  rpnnen2  12780  ruclem3  12787  sqr2irr  12803  dvds2lem  12817  dvdslelem  12849  divalglem8  12875  bitsinv1lem  12908  sadcaddlem  12924  smu01lem  12952  smueqlem  12957  bezoutlem4  12996  algcvga  13025  isprm3  13043  coprm  13055  coprmdvds2  13058  isprm5  13067  rpexp12i  13077  phibndlem  13114  dfphi2  13118  eulerthlem2  13126  odzdvds  13136  iserodd  13164  pclem  13167  pcpremul  13172  pcqcl  13185  pcdvdsb  13197  pcprmpw2  13210  pcaddlem  13212  pcmptcl  13215  pcfac  13223  prmpwdvds  13227  unbenlem  13231  prmreclem1  13239  4sqlem17  13284  vdwmc2  13302  vdwlem9  13312  vdwlem10  13313  vdwlem13  13316  vdwnnlem3  13320  ramcl  13352  mreiincl  13776  pospo  14385  dirge  14637  oddvdsnn0  15137  oddvds  15140  odcl2  15156  gexdvds  15173  sylow1lem1  15187  sylow2alem2  15207  sylow2a  15208  efgi2  15312  efgsrel  15321  efgs1b  15323  cyggex2  15461  pgpfac1lem2  15588  pgpfac1lem3a  15589  pgpfac1lem3  15590  pgpfac1lem5  15592  lssssr  15984  gzrngunitlem  16718  znunit  16799  frgpcyg  16809  lsmcss  16874  obselocv  16910  obslbs  16912  ordtrest2lem  17221  leordtval2  17230  lecldbas  17237  cncls  17292  cncnp  17298  cnpresti  17306  lmcnp  17322  cnt0  17364  isreg2  17395  cmpsublem  17416  cmpsub  17417  tgcmp  17418  dfcon2  17435  1stcfb  17461  2ndcctbss  17471  1stcelcls  17477  islly2  17500  dislly  17513  kgencn2  17542  txcnp  17605  txindis  17619  txcmplem1  17626  txlm  17633  xkohaus  17638  cnmptcom  17663  kqfvima  17715  isr0  17722  fgss2  17859  fbasrn  17869  filuni  17870  ufilmax  17892  isufil2  17893  cfinufil  17913  fmfnfmlem1  17939  fmfnfmlem2  17940  fmfnfmlem4  17942  fmfnfm  17943  fmco  17946  flimopn  17960  hausflim  17966  flimrest  17968  fclsopn  17999  flimfnfcls  18013  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALT  18035  ptcmplem2  18037  cnextcn  18051  symgtgp  18084  divstgplem  18103  tsmsres  18126  tsmsxplem1  18135  isucn2  18262  imasdsf1olem  18356  bldisj  18381  blssps  18407  blss  18408  metcnp3  18523  ngptgp  18630  nrginvrcn  18680  nmoleub  18718  xrsmopn  18796  icccmplem3  18808  reconnlem2  18811  rectbntr0  18816  rescncf  18880  icoopnst  18917  iocopnst  18918  iccpnfcnv  18922  lebnumii  18944  nmoleub2lem  19075  nmhmcn  19081  fgcfil  19177  iscfil3  19179  iscau2  19183  iscau3  19184  iscau4  19185  iscmet3lem2  19198  cfilres  19202  caussi  19203  equivcfil  19205  equivcau  19206  caubl  19213  ivthlem2  19302  ivthlem3  19303  ovoliunlem2  19352  ovoliunnul  19356  ovolicc2lem3  19368  ioombl1lem4  19408  dyadmax  19443  dyadmbl  19445  volsup2  19450  itg2le  19584  itg2const2  19586  itg2seq  19587  itgsplitioo  19682  dvnres  19770  rolle  19827  c1lip1  19834  dvivthlem1  19845  lhop1  19851  dvcnvrelem1  19854  dvfsumrlim  19868  ply1divmo  20011  ig1peu  20047  plypf1  20084  coeaddlem  20120  fta1  20178  quotcan  20179  aalioulem4  20205  ulmcaulem  20263  ulmcn  20268  pilem2  20321  sincosq1lem  20358  sinq12gt0  20368  sinq12ge0  20369  sineq0  20382  tanord1  20392  lognegb  20437  logrec  20614  dcubic  20639  xrlimcnp  20760  o1cxp  20766  ftalem2  20809  ftalem3  20810  fsumdvdscom  20923  chtub  20949  vmasum  20953  bcmono  21014  bposlem3  21023  bposlem7  21027  lgsdir  21067  lgsqrlem2  21079  lgsdchr  21085  lgsquadlem2  21092  2sqlem6  21106  dchrisumlem3  21138  pntrsumbnd2  21214  pntpbnd1  21233  pntibnd  21240  pntlem3  21256  pntleml  21258  redwlk  21559  fargshiftf1  21577  constr3trllem2  21591  4cycl4dv  21607  vdusgra0nedg  21632  usgravd0nedg  21636  eupath2  21655  isgrpo  21737  opidon  21863  vacn  22143  ubthlem2  22326  htthlem  22373  normgt0  22582  shmodsi  22844  spansneleq  23025  h1datomi  23036  pjjsi  23155  nmcexi  23482  pjnormssi  23624  stm1add3i  23703  golem2  23728  cvnsym  23746  dmdmd  23756  mdslmd1lem1  23781  mdslmd1i  23785  mdexchi  23791  atcveq0  23804  superpos  23810  hatomistici  23818  atoml2i  23839  atcvat2i  23843  chirredlem1  23846  atcvat3i  23852  mdsymlem3  23861  mdsymlem5  23863  cdj3lem2b  23893  cdj3i  23897  supssd  24051  resspos  24140  resstos  24141  tpr2rico  24263  xrge0iifcnv  24272  ballotlemfc0  24703  ballotlemfcc  24704  subfacp1lem6  24824  iccllyscon  24890  cvmfolem  24919  cvmliftlem7  24931  cvmliftlem10  24934  ghomf1olem  25058  dedekind  25140  fprodss  25227  fundmpss  25336  dfon2lem3  25355  dfon2lem6  25358  axext4dist  25371  setlikess  25409  trpredtr  25447  trpredmintr  25448  dftrpred3g  25450  trpredrec  25455  frmin  25456  soseq  25468  wfrlem12  25481  frrlem5e  25503  frrlem11  25507  sltval2  25524  sltres  25532  nodenselem4  25552  nodenselem8  25556  nobndlem6  25565  dfrdg4  25703  brbtwn2  25748  colinearalg  25753  axcontlem10  25816  5segofs  25844  cgrextend  25846  segconeu  25849  btwncomim  25851  btwnswapid  25855  btwnintr  25857  btwnexch3  25858  btwndiff  25865  ifscgr  25882  cgrxfr  25893  btwnxfr  25894  lineext  25914  brofs2  25915  linecgr  25919  lineid  25921  idinside  25922  endofsegid  25923  btwnconn1lem13  25937  btwnconn3  25941  onsuct0  26095  limsucncmpi  26099  ltflcei  26140  mblfinlem  26143  mblfinlem2  26144  itg2addnclem  26155  itg2addnclem2  26156  itg2gt0cn  26159  finminlem  26211  nn0prpwlem  26215  cldbnd  26219  clsint2  26222  reftr  26259  fnessref  26263  comppfsc  26277  neibastop3  26281  fgmin  26289  filbcmb  26332  nninfnub  26345  mettrifi  26353  geomcau  26355  istotbnd3  26370  sstotbnd2  26373  ismtybndlem  26405  heibor1lem  26408  heiborlem1  26410  heiborlem8  26417  heiborlem10  26419  heibor  26420  riscer  26494  crngohomfo  26506  keridl  26532  ispridl2  26538  ispridlc  26570  fphpdo  26768  icodiamlt  26773  pellexlem5  26786  pellexlem6  26787  jm2.26lem3  26962  dfac21  27032  unxpwdom3  27124  ordpss  27521  stoweidlem34  27650  ltsubnn0  27973  elfzmlbm  27977  elfzmlbp  27978  ubmelm1fzo  27987  fzo1fzo0n0  27988  swrdnd  28001  swrdswrdlem  28010  swrdswrd  28011  swrdccatin12lem3a  28021  swrdccatin12lem3b  28022  swrdccatin12lem3  28024  swrdccatin12b  28027  swrdccat3a  28030  usgra2adedgspthlem2  28044  usg2wotspth  28081  19.41rg  28348  dvelimvNEW7  29168  dral1NEW7  29199  cbv1hwAUX7  29217  sbiedNEW7  29244  sbequiNEW7  29282  cbv1hOLD7  29403  lsatcveq0  29515  eqlkr3  29584  atlatmstc  29802  atlrelat1  29804  hlrelat2  29885  intnatN  29889  cvrexchlem  29901  cvratlem  29903  cvrat2  29911  atltcvr  29917  cvrat3  29924  cvrat4  29925  ps-1  29959  ps-2  29960  lplnnle2at  30023  lvolnle3at  30064  2llnma3r  30270  cdlemblem  30275  pmapjoin  30334  elpcliN  30375  lhpmcvr4N  30508  4atexlemnclw  30552  trlnidatb  30659  cdlemc4  30676  cdlemd3  30682  cdleme3g  30716  cdleme7d  30728  cdleme11c  30743  cdleme11dN  30744  cdleme21b  30808  cdleme21c  30809  cdleme21i  30817  cdleme22b  30823  cdleme35fnpq  30931  cdlemf1  31043  trlord  31051  cdlemg6c  31102  dihglblem6  31823  dochlkr  31868  dochkrshp  31869  dihjat1lem  31911  dochexmidlem5  31947  dochexmidlem8  31950

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8