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  a2andOLD  812  ax12v  1841  alrimdd  1866  axc112  1923  nfeqf2  2027  equveliOLD  2075  sbequi  2102  dral1-o  2219  ax12indalem  2261  ax12inda2ALT  2262  2eu1  2362  axext3  2423  trel3  4538  poss  4792  sess2  4838  wefrc  4863  wereu2  4866  funun  5620  ssimaex  5923  f1imass  6157  soisoi  6209  isores3  6216  isofrlem  6221  isoselem  6222  weniso  6235  oninton  6620  orduniorsuc  6650  limuni3  6672  tfindsg  6680  limom  6700  f1o2ndf1  6893  soxp  6898  extmptsuppeq  6926  smoel  7033  smogt  7040  tfrlem9  7056  tz7.49  7112  seqomlem1  7117  odi  7230  omass  7231  omeulem2  7234  oeordsuc  7245  oeeulem  7252  ertr  7328  swoord2  7343  ecopovtrn  7416  domtriord  7665  onomeneq  7709  unxpdomlem2  7727  isinf  7735  pssnn  7740  findcard3  7765  frfi  7767  unblem3  7776  dffi3  7893  en3lplem1  8034  inf3lem3  8050  inf3lem5  8052  noinfep  8079  cantnfle  8093  cantnfp1lem3  8102  cantnfleOLD  8123  cantnfp1lem3OLD  8128  rankxpsuc  8303  tcrank  8305  ficardom  8345  carduni  8365  infxpenlem  8394  dfac8alem  8413  ac10ct  8418  ween  8419  alephdom  8465  alephle  8472  iscard3  8477  alephfp  8492  cdainf  8575  pwsdompw  8587  infdif  8592  cfslbn  8650  cofsmo  8652  cfsmolem  8653  cfcof  8657  fin1a2s  8797  domtriomlem  8825  ac6num  8862  zorn2lem3  8881  axdclem2  8903  imadomg  8915  iundom2g  8918  ficard  8943  fpwwe2lem8  9018  fpwwe2  9024  gchaclem  9059  tskr1om2  9149  inar1  9156  tskord  9161  tskuni  9164  grudomon  9198  grur1a  9200  grur1  9201  addnidpi  9282  ltexnq  9356  genpnnp  9386  addclprlem2  9398  mulclprlem  9400  psslinpr  9412  ltaddpr2  9416  ltexprlem6  9422  ltexprlem7  9423  addcanpr  9427  mulgt0sr  9485  map2psrpr  9490  supsrlem  9491  axrrecex  9543  letr  9681  dedekind  9747  recex  10188  lemul12b  10406  mulgt1  10408  ledivmulOLD  10426  fimaxre2  10498  lbreu  10500  nnrecgt0  10580  nnunb  10798  bndndx  10801  zeo  10955  uzind  10961  fzind  10969  fnn0ind  10970  suprfinzcl  10985  suprzcl2  11183  zmax  11190  rpnnen1lem5  11223  xrletr  11372  qbtwnre  11409  qsqueeze  11411  qextltlem  11412  xralrple  11415  xlesubadd  11466  supxrunb1  11522  icoshft  11653  fzen  11714  elfz1b  11759  elfz0fzfz0  11790  elfzmlbmOLD  11796  elfzmlbp  11797  fzo1fzo0n0  11846  elfzo0z  11847  fzofzim  11851  elfzodifsumelfzo  11864  ssfzoulel  11888  modadd1  12015  modmul1  12022  uzrdgfni  12051  fsuppmapnn0fiub0  12081  fsuppmapnn0ub  12083  fsuppmapnn0fz  12084  seqcl2  12107  seqfveq2  12111  seqshft2  12115  monoord  12119  seqsplit  12122  seqf1olem1  12128  seqf1olem2  12129  seqid2  12135  seqhomo  12136  expnbnd  12277  faclbnd4lem4  12356  seqcoll  12494  swrdnd  12639  swrdvalodm2  12646  swrdswrdlem  12666  swrdswrd  12667  reuccats1lem  12687  swrdccatin12lem2a  12692  swrdccatin12lem2b  12693  swrdccatin12lem3  12697  swrdccat3a  12701  swrdccat3blem  12702  repswswrd  12738  swrd2lsw  12872  sqeqd  12981  sqrmo  13067  cau3lem  13169  limsupbnd2  13288  lo1bdd2  13329  climuni  13357  rlimcn2  13395  mulcn2  13400  o1of2  13417  rlimo1  13421  lo1le  13456  isercolllem1  13469  iseralt  13489  cvgrat  13674  fprodss  13737  rpnnen2  13941  ruclem3  13948  sqrt2irr  13964  dvds2lem  13978  dvdslelem  14012  divalglem8  14040  bitsinv1lem  14073  sadcaddlem  14089  smu01lem  14117  smueqlem  14122  bezoutlem4  14161  algcvga  14190  isprm3  14208  coprm  14223  coprmdvds2  14226  isprm5  14235  rpexp12i  14245  phibndlem  14282  dfphi2  14286  eulerthlem2  14294  odzdvds  14304  iserodd  14341  pclem  14344  pcpremul  14349  pcqcl  14362  pcdvdsb  14374  pcprmpw2  14387  pcaddlem  14389  pcmptcl  14392  pcfac  14400  prmpwdvds  14404  unbenlem  14408  prmreclem1  14416  4sqlem17  14461  vdwmc2  14479  vdwlem9  14489  vdwlem10  14490  vdwlem13  14493  vdwnnlem3  14497  ramcl  14529  mreiincl  14975  pospo  15582  dirge  15846  gsmsymgrfixlem1  16431  oddvdsnn0  16547  oddvds  16550  odcl2  16566  gexdvds  16583  sylow1lem1  16597  sylow2alem2  16617  sylow2a  16618  efgi2  16722  efgsrel  16731  efgs1b  16733  cyggex2  16878  telgsums  17001  pgpfac1lem2  17105  pgpfac1lem3a  17106  pgpfac1lem3  17107  pgpfac1lem5  17109  lssssr  17578  cply1mul  18314  gsummoncoe1  18325  gzrngunitlem  18461  znunit  18580  frgpcyg  18590  lsmcss  18701  obselocv  18737  obslbs  18739  scmataddcl  18996  scmatsubcl  18997  cpmatacl  19195  cpmatinvcl  19196  cpmatmcllem  19197  m2cpminvid2lem  19233  mp2pm2mplem4  19288  pm2mp  19304  chfacfisf  19333  chfacfisfcpmat  19334  chfacfscmul0  19337  chfacfpmmul0  19341  cayhamlem4  19367  ordtrest2lem  19682  leordtval2  19691  lecldbas  19698  cncls  19753  cncnp  19759  cnpresti  19767  lmcnp  19783  cnt0  19825  isreg2  19856  cmpsublem  19877  cmpsub  19878  tgcmp  19879  bwth  19888  bwthOLD  19889  dfcon2  19898  1stcfb  19924  2ndcctbss  19934  1stcelcls  19940  islly2  19963  dislly  19976  reftr  19993  comppfsc  20011  kgencn2  20036  txcnp  20099  txindis  20113  txcmplem1  20120  txlm  20127  xkohaus  20132  cnmptcom  20157  kqfvima  20209  isr0  20216  fgss2  20353  fbasrn  20363  filuni  20364  ufilmax  20386  isufil2  20387  cfinufil  20407  fmfnfmlem1  20433  fmfnfmlem2  20434  fmfnfmlem4  20436  fmfnfm  20437  fmco  20440  flimopn  20454  hausflim  20460  flimrest  20462  fclsopn  20493  flimfnfcls  20507  alexsubALTlem2  20526  alexsubALTlem3  20527  alexsubALT  20529  ptcmplem2  20531  cnextcn  20545  symgtgp  20578  qustgplem  20597  tsmsresOLD  20623  tsmsres  20624  tsmsxplem1  20633  isucn2  20760  imasdsf1olem  20854  bldisj  20879  blssps  20905  blss  20906  metcnp3  21021  ngptgp  21128  nrginvrcn  21178  nmoleub  21216  xrsmopn  21295  icccmplem3  21307  reconnlem2  21310  rectbntr0  21315  rescncf  21379  iocopnst  21418  iccpnfcnv  21422  lebnumii  21444  nmoleub2lem  21575  nmhmcn  21581  fgcfil  21688  iscfil3  21690  iscau2  21694  iscau3  21695  iscau4  21696  iscmet3lem2  21709  cfilres  21713  caussi  21714  equivcfil  21716  equivcau  21717  ivthlem2  21842  ivthlem3  21843  ovoliunlem2  21892  ovoliunnul  21896  ovolicc2lem3  21908  ioombl1lem4  21949  dyadmax  21985  dyadmbl  21987  volsup2  21992  itg2le  22124  itg2const2  22126  itg2seq  22127  itgsplitioo  22222  dvnres  22312  rolle  22369  c1lip1  22376  dvivthlem1  22387  lhop1  22393  dvcnvrelem1  22396  dvfsumrlim  22410  ply1divmo  22514  ig1peu  22550  plypf1  22587  coeaddlem  22624  fta1  22682  quotcan  22683  aalioulem4  22709  ulmcaulem  22767  ulmcn  22772  pilem2  22825  sincosq1lem  22868  sinq12gt0  22878  sinq12ge0  22879  sineq0  22892  tanord1  22902  lognegb  22952  logrec  23129  dcubic  23155  xrlimcnp  23276  o1cxp  23282  ftalem2  23325  ftalem3  23326  fsumdvdscom  23439  chtub  23465  vmasum  23469  bcmono  23530  bposlem3  23539  bposlem7  23543  lgsdir  23583  lgsqrlem2  23595  lgsdchr  23601  lgsquadlem2  23608  2sqlem6  23622  dchrisumlem3  23654  pntrsumbnd2  23730  pntpbnd1  23749  pntibnd  23756  pntlem3  23772  pntleml  23774  brbtwn2  24186  colinearalg  24191  axcontlem10  24254  redwlk  24586  usgra2adedgspthlem2  24590  fargshiftf1  24615  constr3trllem2  24629  4cycl4dv  24645  usg2wlkeq  24686  wwlknred  24701  wwlknextbi  24703  wwlkm1edg  24713  clwlkswlks  24736  clwlkisclwwlklem2fv2  24761  clwlkisclwwlklem2a  24763  clwlkisclwwlklem1  24765  clwwlkf  24772  clwwlkext2edg  24780  wwlksubclwwlk  24782  clwwisshclwwlem1  24783  usg2wotspth  24862  vdusgra0nedg  24886  usgravd0nedg  24896  usgravd00  24897  eupath2  24958  frgraregorufrg  25050  numclwwlkovf2ex  25064  numclwlk1lem2foa  25069  numclwlk1lem2fo  25073  ex-natded5.3-2  25107  isgrpo  25176  opidonOLD  25302  vacn  25582  ubthlem2  25765  htthlem  25812  normgt0  26022  shmodsi  26285  spansneleq  26466  h1datomi  26477  pjjsi  26596  nmcexi  26923  pjnormssi  27065  stm1add3i  27144  golem2  27169  cvnsym  27187  dmdmd  27197  mdslmd1lem1  27222  mdslmd1i  27226  mdexchi  27232  atcveq0  27245  superpos  27251  hatomistici  27259  atoml2i  27280  atcvat2i  27284  chirredlem1  27287  atcvat3i  27293  mdsymlem3  27302  mdsymlem5  27304  cdj3lem2b  27334  cdj3i  27338  supssd  27505  2sqmod  27614  resspos  27625  resstos  27626  submarchi  27708  tpr2rico  27872  ordtrest2NEWlem  27882  xrge0iifcnv  27893  eulerpartlemb  28285  ballotlemfc0  28409  ballotlemfcc  28410  subfacp1lem6  28607  iccllyscon  28673  cvmfolem  28702  cvmliftlem7  28714  cvmliftlem10  28717  ghomf1olem  29012  fundmpss  29172  dfon2lem3  29193  dfon2lem6  29196  axext4dist  29209  setlikess  29251  trpredtr  29289  trpredmintr  29290  dftrpred3g  29292  trpredrec  29297  frmin  29298  soseq  29310  wfrlem12  29330  frrlem5e  29371  frrlem11  29375  sltval2  29392  sltres  29400  nodenselem4  29420  nodenselem8  29424  nobndlem6  29433  dfrdg4  29576  5segofs  29632  cgrextend  29634  segconeu  29637  btwncomim  29639  btwnswapid  29643  btwnintr  29645  btwnexch3  29646  btwndiff  29653  ifscgr  29670  cgrxfr  29681  btwnxfr  29682  lineext  29702  brofs2  29703  linecgr  29707  lineid  29709  idinside  29710  endofsegid  29711  btwnconn1lem13  29725  btwnconn3  29729  onsuct0  29882  limsucncmpi  29886  wl-aetr  29959  fin2so  30016  tan2h  30023  heicant  30025  mblfinlem2  30028  mblfinlem3  30029  itg2addnclem  30042  itg2addnclem2  30043  itg2gt0cn  30046  ftc1anclem5  30070  ftc1anclem6  30071  finminlem  30112  nn0prpwlem  30116  cldbnd  30120  clsint2  30123  fnessref  30151  neibastop3  30156  fgmin  30164  filbcmb  30207  nninfnub  30220  mettrifi  30226  geomcau  30228  istotbnd3  30243  sstotbnd2  30246  ismtybndlem  30278  heibor1lem  30281  heiborlem1  30283  heiborlem8  30290  heiborlem10  30292  heibor  30293  riscer  30367  crngohomfo  30379  keridl  30405  ispridl2  30411  ispridlc  30443  ac6s6  30556  fphpdo  30727  icodiamlt  30732  pellexlem5  30745  pellexlem6  30746  jm2.26lem3  30919  dfac21  30988  unxpwdom3  31017  ordpss  31314  stoweidlem34  31770  ralralimp  32249  zm1nn  32279  ltsubnn0  32281  elfz2z  32285  usgedgimp  32357  usgvincvad  32358  usgedgimpALT  32360  usgvincvadALT  32361  ztprmneprm  32804  lcosslsp  32909  lindslinindsimp1  32928  lindslinindsimp2lem5  32933  snlindsntor  32942  19.41rg  33191  bj-exalimi  34108  lsatcveq0  34632  eqlkr3  34701  atlatmstc  34919  atlrelat1  34921  hlrelat2  35002  intnatN  35006  cvrexchlem  35018  cvratlem  35020  cvrat2  35028  atltcvr  35034  cvrat3  35041  cvrat4  35042  ps-1  35076  ps-2  35077  lplnnle2at  35140  lvolnle3at  35181  2llnma3r  35387  cdlemblem  35392  pmapjoin  35451  elpcliN  35492  lhpmcvr4N  35625  4atexlemnclw  35669  trlnidatb  35777  cdlemc4  35794  cdlemd3  35800  cdleme3g  35834  cdleme7d  35846  cdleme11c  35861  cdleme11dN  35862  cdleme21b  35927  cdleme21c  35928  cdleme21i  35936  cdleme22b  35942  cdleme35fnpq  36050  cdlemf1  36162  trlord  36170  cdlemg6c  36221  dihglblem6  36942  dochlkr  36987  dochkrshp  36988  dihjat1lem  37030  dochexmidlem5  37066  dochexmidlem8  37069