Theorem syld 44

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

Notice that syld 44 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 22 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 25	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	1, 3	mpdd 40	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  55  sylsyld  56  nsyld  140  pm2.61d  158  sylibd  214  sylbid  215  sylibrd  234  sylbird  235  syland  481  alrimdd  1816  axc112  1872  cbv1hOLD  1972  nfeqf2  1998  equveliOLD  2046  sbequi  2073  sbiedOLD  2110  dral1-o  2211  ax12indalem  2253  ax12inda2ALT  2254  2eu1  2371  trel3  4491  poss  4741  sess2  4787  wefrc  4812  wereu2  4815  ordelord  4839  funun  5558  ssimaex  5855  f1imass  6076  soisoi  6118  isores3  6125  isofrlem  6130  isoselem  6131  weniso  6144  oninton  6511  orduniorsuc  6541  limuni3  6563  tfindsg  6571  limom  6591  f1dmex  6647  f1o2ndf1  6780  soxp  6785  extmptsuppeq  6813  smoel  6921  smogt  6928  tfrlem9  6944  tz7.49  7000  seqomlem1  7005  odi  7118  omass  7119  omeulem2  7122  oeordsuc  7133  oeeulem  7140  ertr  7216  swoord2  7231  ecopovtrn  7303  domtriord  7557  2pwuninel  7566  onomeneq  7601  unxpdomlem2  7619  isinf  7627  pssnn  7632  findcard3  7656  frfi  7658  unblem3  7667  dffi3  7782  en3lplem1  7921  inf3lem3  7937  inf3lem5  7939  noinfep  7966  cantnfle  7980  cantnfp1lem3  7989  cantnfleOLD  8010  cantnfp1lem3OLD  8015  rankxpsuc  8190  tcrank  8192  ficardom  8232  carduni  8252  infxpenlem  8281  dfac8alem  8300  ac10ct  8305  ween  8306  alephdom  8352  alephle  8359  iscard3  8364  alephfp  8379  cdainf  8462  pwsdompw  8474  infdif  8479  cfslbn  8537  cofsmo  8539  cfsmolem  8540  cfcof  8544  fin1a2s  8684  domtriomlem  8712  ac6num  8749  zorn2lem3  8768  axdclem2  8790  imadomg  8802  iundom2g  8805  ficard  8830  fpwwe2lem8  8905  fpwwe2  8911  gchaclem  8946  tskr1om2  9036  inar1  9043  tskord  9048  tskuni  9051  grudomon  9085  grur1a  9087  grur1  9088  addnidpi  9171  ltexnq  9245  genpnnp  9275  addclprlem2  9287  mulclprlem  9289  psslinpr  9301  ltaddpr2  9305  ltexprlem6  9311  ltexprlem7  9312  addcanpr  9316  mulgt0sr  9373  map2psrpr  9378  supsrlem  9379  axrrecex  9431  letr  9569  dedekind  9634  recex  10069  lemul12b  10287  mulgt1  10289  ledivmulOLD  10307  fimaxre2  10379  lbreu  10381  nnrecgt0  10460  nnunb  10676  bndndx  10679  zeo  10828  uzind  10834  fzind  10841  fnn0ind  10842  lbzbi  11044  suprzcl2  11046  zmax  11051  rpnnen1lem5  11084  xrletr  11233  qbtwnre  11270  qsqueeze  11272  qextltlem  11273  xralrple  11276  xlesubadd  11327  supxrunb1  11383  icoshft  11508  fzen  11568  elfz0fzfz0  11586  elfzmlbm  11591  elfzmlbp  11592  elfz1b  11628  fzo1fzo0n0  11689  elfzo0z  11690  fzofzim  11694  elfzodifsumelfzo  11705  ssfzoulel  11722  modadd1  11846  modmul1  11853  uzrdgfni  11882  seqcl2  11925  seqfveq2  11929  seqshft2  11933  monoord  11937  seqsplit  11940  seqf1olem1  11946  seqf1olem2  11947  seqid2  11953  seqhomo  11954  expnbnd  12094  faclbnd4lem4  12173  seqcoll  12318  swrdnd  12428  swrdvalodm2  12435  swrdswrdlem  12455  swrdswrd  12456  swrdccatin12lem2a  12478  swrdccatin12lem2b  12479  swrdccatin12lem3  12483  swrdccat3a  12487  swrdccat3blem  12488  repswswrd  12524  swrd2lsw  12654  sqeqd  12757  sqrmo  12843  cau3lem  12944  limsupbnd2  13063  lo1bdd2  13104  climuni  13132  rlimcn2  13170  mulcn2  13175  o1of2  13192  rlimo1  13196  lo1le  13231  isercolllem1  13244  iseralt  13264  isumrpcl  13408  cvgrat  13445  rpnnen2  13610  ruclem3  13617  sqr2irr  13633  dvds2lem  13647  dvdslelem  13679  divalglem8  13706  bitsinv1lem  13739  sadcaddlem  13755  smu01lem  13783  smueqlem  13788  bezoutlem4  13827  algcvga  13856  isprm3  13874  coprm  13888  coprmdvds2  13891  isprm5  13900  rpexp12i  13910  phibndlem  13947  dfphi2  13951  eulerthlem2  13959  odzdvds  13969  iserodd  14004  pclem  14007  pcpremul  14012  pcqcl  14025  pcdvdsb  14037  pcprmpw2  14050  pcaddlem  14052  pcmptcl  14055  pcfac  14063  prmpwdvds  14067  unbenlem  14071  prmreclem1  14079  4sqlem17  14124  vdwmc2  14142  vdwlem9  14152  vdwlem10  14153  vdwlem13  14156  vdwnnlem3  14160  ramcl  14192  mreiincl  14636  pospo  15245  dirge  15509  gsmsymgrfixlem1  16034  oddvdsnn0  16151  oddvds  16154  odcl2  16170  gexdvds  16187  sylow1lem1  16201  sylow2alem2  16221  sylow2a  16222  efgi2  16326  efgsrel  16335  efgs1b  16337  cyggex2  16477  pgpfac1lem2  16681  pgpfac1lem3a  16682  pgpfac1lem3  16683  pgpfac1lem5  16685  lssssr  17140  gzrngunitlem  17986  znunit  18105  frgpcyg  18115  lsmcss  18226  obselocv  18262  obslbs  18264  ordtrest2lem  18923  leordtval2  18932  lecldbas  18939  cncls  18994  cncnp  19000  cnpresti  19008  lmcnp  19024  cnt0  19066  isreg2  19097  cmpsublem  19118  cmpsub  19119  tgcmp  19120  bwth  19129  bwthOLD  19130  dfcon2  19139  1stcfb  19165  2ndcctbss  19175  1stcelcls  19181  islly2  19204  dislly  19217  kgencn2  19246  txcnp  19309  txindis  19323  txcmplem1  19330  txlm  19337  xkohaus  19342  cnmptcom  19367  kqfvima  19419  isr0  19426  fgss2  19563  fbasrn  19573  filuni  19574  ufilmax  19596  isufil2  19597  cfinufil  19617  fmfnfmlem1  19643  fmfnfmlem2  19644  fmfnfmlem4  19646  fmfnfm  19647  fmco  19650  flimopn  19664  hausflim  19670  flimrest  19672  fclsopn  19703  flimfnfcls  19717  alexsubALTlem2  19736  alexsubALTlem3  19737  alexsubALT  19739  ptcmplem2  19741  cnextcn  19755  symgtgp  19788  divstgplem  19807  tsmsresOLD  19833  tsmsres  19834  tsmsxplem1  19843  isucn2  19970  imasdsf1olem  20064  bldisj  20089  blssps  20115  blss  20116  metcnp3  20231  ngptgp  20338  nrginvrcn  20388  nmoleub  20426  xrsmopn  20505  icccmplem3  20517  reconnlem2  20520  rectbntr0  20525  rescncf  20589  icoopnst  20627  iocopnst  20628  iccpnfcnv  20632  lebnumii  20654  nmoleub2lem  20785  nmhmcn  20791  fgcfil  20898  iscfil3  20900  iscau2  20904  iscau3  20905  iscau4  20906  iscmet3lem2  20919  cfilres  20923  caussi  20924  equivcfil  20926  equivcau  20927  caubl  20934  ivthlem2  21052  ivthlem3  21053  ovoliunlem2  21102  ovoliunnul  21106  ovolicc2lem3  21118  ioombl1lem4  21158  dyadmax  21194  dyadmbl  21196  volsup2  21201  itg2le  21333  itg2const2  21335  itg2seq  21336  itgsplitioo  21431  dvnres  21521  rolle  21578  c1lip1  21585  dvivthlem1  21596  lhop1  21602  dvcnvrelem1  21605  dvfsumrlim  21619  ply1divmo  21723  ig1peu  21759  plypf1  21796  coeaddlem  21832  fta1  21890  quotcan  21891  aalioulem4  21917  ulmcaulem  21975  ulmcn  21980  pilem2  22033  sincosq1lem  22075  sinq12gt0  22085  sinq12ge0  22086  sineq0  22099  tanord1  22109  lognegb  22154  logrec  22331  dcubic  22357  xrlimcnp  22478  o1cxp  22484  ftalem2  22527  ftalem3  22528  fsumdvdscom  22641  chtub  22667  vmasum  22671  bcmono  22732  bposlem3  22741  bposlem7  22745  lgsdir  22785  lgsqrlem2  22797  lgsdchr  22803  lgsquadlem2  22810  2sqlem6  22824  dchrisumlem3  22856  pntrsumbnd2  22932  pntpbnd1  22951  pntibnd  22958  pntlem3  22974  pntleml  22976  brbtwn2  23286  colinearalg  23291  axcontlem10  23354  redwlk  23640  fargshiftf1  23658  constr3trllem2  23672  4cycl4dv  23688  vdusgra0nedg  23713  usgravd0nedg  23717  eupath2  23736  ex-natded5.3-2  23750  isgrpo  23818  opidon  23944  vacn  24224  ubthlem2  24407  htthlem  24454  normgt0  24664  shmodsi  24927  spansneleq  25108  h1datomi  25119  pjjsi  25238  nmcexi  25565  pjnormssi  25707  stm1add3i  25786  golem2  25811  cvnsym  25829  dmdmd  25839  mdslmd1lem1  25864  mdslmd1i  25868  mdexchi  25874  atcveq0  25887  superpos  25893  hatomistici  25901  atoml2i  25922  atcvat2i  25926  chirredlem1  25929  atcvat3i  25935  mdsymlem3  25944  mdsymlem5  25946  cdj3lem2b  25976  cdj3i  25980  supssd  26138  resspos  26254  resstos  26255  submarchi  26337  tpr2rico  26476  ordtrest2NEWlem  26486  xrge0iifcnv  26497  eulerpartlemb  26885  ballotlemfc0  27009  ballotlemfcc  27010  subfacp1lem6  27207  iccllyscon  27273  cvmfolem  27302  cvmliftlem7  27314  cvmliftlem10  27317  ghomf1olem  27447  fprodss  27595  fundmpss  27711  dfon2lem3  27732  dfon2lem6  27735  axext4dist  27748  setlikess  27790  trpredtr  27828  trpredmintr  27829  dftrpred3g  27831  trpredrec  27836  frmin  27837  soseq  27849  wfrlem12  27869  frrlem5e  27910  frrlem11  27914  sltval2  27931  sltres  27939  nodenselem4  27959  nodenselem8  27963  nobndlem6  27972  dfrdg4  28115  5segofs  28171  cgrextend  28173  segconeu  28176  btwncomim  28178  btwnswapid  28182  btwnintr  28184  btwnexch3  28185  btwndiff  28192  ifscgr  28209  cgrxfr  28220  btwnxfr  28221  lineext  28241  brofs2  28242  linecgr  28246  lineid  28248  idinside  28249  endofsegid  28250  btwnconn1lem13  28264  btwnconn3  28268  onsuct0  28421  limsucncmpi  28425  wl-aetr  28497  fin2so  28554  ltflcei  28557  tan2h  28562  heicant  28564  mblfinlem2  28567  mblfinlem3  28568  itg2addnclem  28581  itg2addnclem2  28582  itg2gt0cn  28585  ftc1anclem5  28609  ftc1anclem6  28610  finminlem  28651  nn0prpwlem  28655  cldbnd  28659  clsint2  28662  reftr  28699  fnessref  28703  comppfsc  28717  neibastop3  28721  fgmin  28729  filbcmb  28772  nninfnub  28785  mettrifi  28791  geomcau  28793  istotbnd3  28808  sstotbnd2  28811  ismtybndlem  28843  heibor1lem  28846  heiborlem1  28848  heiborlem8  28855  heiborlem10  28857  heibor  28858  riscer  28932  crngohomfo  28944  keridl  28970  ispridl2  28976  ispridlc  29008  ac6s6  29122  fphpdo  29294  icodiamlt  29299  pellexlem5  29312  pellexlem6  29313  jm2.26lem3  29488  dfac21  29557  unxpwdom3  29586  ordpss  29845  stoweidlem34  29967  ralralimp  30257  ltsubnn0  30320  elfz2z  30336  usg2wlkeq  30427  usgra2adedgspthlem2  30442  wwlknred  30493  wwlknextbi  30495  wwlkm1edg  30505  usg2wotspth  30541  clwlkswlks  30561  clwlkisclwwlklem2fv2  30583  clwlkisclwwlklem2a  30585  clwlkisclwwlklem1  30587  clwwlkf  30594  clwwlkext2edg  30602  wwlksubclwwlk  30604  zm1nn  30606  clwwisshclwwlem1  30607  usgravd00  30676  frgraregorufrg  30803  numclwwlkovf2ex  30817  numclwlk1lem2foa  30822  numclwlk1lem2fo  30826  a2and  30854  ztprmneprm  30877  suprfinzcl  30883  fsuppmapnn0ub  30934  fsuppmapnn0fz  30935  fsuppmapnn0fiub0  30939  telescgsum  30955  gsummoncoe1  30985  cply1mul  30993  lcosslsp  31079  lindslinindsimp1  31098  lindslinindsimp2lem5  31103  snlindsntor  31112  cpmatacl  31179  cpmatinvcl  31180  cpmatmcllem  31181  m2pminv2lem  31212  mp2pm2mplem4  31264  pmat2matp  31279  chfacfisf  31308  chfacfisfcpmat  31309  chfacfscmul0  31312  chfacfpmmul0  31316  chcoeffeq  31341  cayhamlem4  31343  19.41rg  31559  bj-exalimi  32468  lsatcveq0  32983  eqlkr3  33052  atlatmstc  33270  atlrelat1  33272  hlrelat2  33353  intnatN  33357  cvrexchlem  33369  cvratlem  33371  cvrat2  33379  atltcvr  33385  cvrat3  33392  cvrat4  33393  ps-1  33427  ps-2  33428  lplnnle2at  33491  lvolnle3at  33532  2llnma3r  33738  cdlemblem  33743  pmapjoin  33802  elpcliN  33843  lhpmcvr4N  33976  4atexlemnclw  34020  trlnidatb  34127  cdlemc4  34144  cdlemd3  34150  cdleme3g  34184  cdleme7d  34196  cdleme11c  34211  cdleme11dN  34212  cdleme21b  34276  cdleme21c  34277  cdleme21i  34285  cdleme22b  34291  cdleme35fnpq  34399  cdlemf1  34511  trlord  34519  cdlemg6c  34570  dihglblem6  35291  dochlkr  35336  dochkrshp  35337  dihjat1lem  35379  dochexmidlem5  35415  dochexmidlem8  35418