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  810  ax12v  1804  alrimdd  1828  axc112  1884  cbv1hOLD  1988  nfeqf2  2014  equveliOLD  2062  sbequi  2089  sbiedOLD  2126  dral1-o  2226  ax12indalem  2268  ax12inda2ALT  2269  2eu1  2386  axext3  2447  trel3  4548  poss  4802  sess2  4848  wefrc  4873  wereu2  4876  ordelord  4900  funun  5628  ssimaex  5930  f1imass  6158  soisoi  6210  isores3  6217  isofrlem  6222  isoselem  6223  weniso  6236  oninton  6613  orduniorsuc  6643  limuni3  6665  tfindsg  6673  limom  6693  f1dmex  6751  f1o2ndf1  6888  soxp  6893  extmptsuppeq  6921  smoel  7028  smogt  7035  tfrlem9  7051  tz7.49  7107  seqomlem1  7112  odi  7225  omass  7226  omeulem2  7229  oeordsuc  7240  oeeulem  7247  ertr  7323  swoord2  7338  ecopovtrn  7411  domtriord  7660  2pwuninel  7669  onomeneq  7704  unxpdomlem2  7722  isinf  7730  pssnn  7735  findcard3  7759  frfi  7761  unblem3  7770  dffi3  7887  en3lplem1  8027  inf3lem3  8043  inf3lem5  8045  noinfep  8072  cantnfle  8086  cantnfp1lem3  8095  cantnfleOLD  8116  cantnfp1lem3OLD  8121  rankxpsuc  8296  tcrank  8298  ficardom  8338  carduni  8358  infxpenlem  8387  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  9011  fpwwe2  9017  gchaclem  9052  tskr1om2  9142  inar1  9149  tskord  9154  tskuni  9157  grudomon  9191  grur1a  9193  grur1  9194  addnidpi  9275  ltexnq  9349  genpnnp  9379  addclprlem2  9391  mulclprlem  9393  psslinpr  9405  ltaddpr2  9409  ltexprlem6  9415  ltexprlem7  9416  addcanpr  9420  mulgt0sr  9478  map2psrpr  9483  supsrlem  9484  axrrecex  9536  letr  9674  dedekind  9739  recex  10177  lemul12b  10395  mulgt1  10397  ledivmulOLD  10415  fimaxre2  10487  lbreu  10489  nnrecgt0  10569  nnunb  10787  bndndx  10790  zeo  10942  uzind  10948  fzind  10955  fnn0ind  10956  suprfinzcl  10971  lbzbi  11166  suprzcl2  11168  zmax  11175  rpnnen1lem5  11208  xrletr  11357  qbtwnre  11394  qsqueeze  11396  qextltlem  11397  xralrple  11400  xlesubadd  11451  supxrunb1  11507  icoshft  11638  fzen  11699  elfz1b  11744  elfz0fzfz0  11773  elfzmlbm  11778  elfzmlbp  11779  fzo1fzo0n0  11828  elfzo0z  11829  fzofzim  11833  elfzodifsumelfzo  11846  ssfzoulel  11870  modadd1  11996  modmul1  12003  uzrdgfni  12032  fsuppmapnn0fiub0  12062  fsuppmapnn0ub  12064  fsuppmapnn0fz  12065  seqcl2  12088  seqfveq2  12092  seqshft2  12096  monoord  12100  seqsplit  12103  seqf1olem1  12109  seqf1olem2  12110  seqid2  12116  seqhomo  12117  expnbnd  12257  faclbnd4lem4  12336  seqcoll  12472  swrdnd  12614  swrdvalodm2  12621  swrdswrdlem  12641  swrdswrd  12642  reuccats1lem  12662  swrdccatin12lem2a  12667  swrdccatin12lem2b  12668  swrdccatin12lem3  12672  swrdccat3a  12676  swrdccat3blem  12677  repswswrd  12713  swrd2lsw  12847  sqeqd  12956  sqrmo  13042  cau3lem  13143  limsupbnd2  13262  lo1bdd2  13303  climuni  13331  rlimcn2  13369  mulcn2  13374  o1of2  13391  rlimo1  13395  lo1le  13430  isercolllem1  13443  iseralt  13463  isumrpcl  13611  cvgrat  13648  rpnnen2  13813  ruclem3  13820  sqrt2irr  13836  dvds2lem  13850  dvdslelem  13882  divalglem8  13910  bitsinv1lem  13943  sadcaddlem  13959  smu01lem  13987  smueqlem  13992  bezoutlem4  14031  algcvga  14060  isprm3  14078  coprm  14093  coprmdvds2  14096  isprm5  14105  rpexp12i  14115  phibndlem  14152  dfphi2  14156  eulerthlem2  14164  odzdvds  14174  iserodd  14211  pclem  14214  pcpremul  14219  pcqcl  14232  pcdvdsb  14244  pcprmpw2  14257  pcaddlem  14259  pcmptcl  14262  pcfac  14270  prmpwdvds  14274  unbenlem  14278  prmreclem1  14286  4sqlem17  14331  vdwmc2  14349  vdwlem9  14359  vdwlem10  14360  vdwlem13  14363  vdwnnlem3  14367  ramcl  14399  mreiincl  14844  pospo  15453  dirge  15717  gsmsymgrfixlem1  16244  oddvdsnn0  16361  oddvds  16364  odcl2  16380  gexdvds  16397  sylow1lem1  16411  sylow2alem2  16431  sylow2a  16432  efgi2  16536  efgsrel  16545  efgs1b  16547  cyggex2  16687  telgsums  16810  pgpfac1lem2  16913  pgpfac1lem3a  16914  pgpfac1lem3  16915  pgpfac1lem5  16917  lssssr  17379  cply1mul  18103  gsummoncoe1  18114  gzrngunitlem  18247  znunit  18366  frgpcyg  18376  lsmcss  18487  obselocv  18523  obslbs  18525  scmataddcl  18782  scmatsubcl  18783  cpmatacl  18981  cpmatinvcl  18982  cpmatmcllem  18983  m2cpminvid2lem  19019  mp2pm2mplem4  19074  pm2mp  19090  chfacfisf  19119  chfacfisfcpmat  19120  chfacfscmul0  19123  chfacfpmmul0  19127  cayhamlem4  19153  ordtrest2lem  19467  leordtval2  19476  lecldbas  19483  cncls  19538  cncnp  19544  cnpresti  19552  lmcnp  19568  cnt0  19610  isreg2  19641  cmpsublem  19662  cmpsub  19663  tgcmp  19664  bwth  19673  bwthOLD  19674  dfcon2  19683  1stcfb  19709  2ndcctbss  19719  1stcelcls  19725  islly2  19748  dislly  19761  kgencn2  19790  txcnp  19853  txindis  19867  txcmplem1  19874  txlm  19881  xkohaus  19886  cnmptcom  19911  kqfvima  19963  isr0  19970  fgss2  20107  fbasrn  20117  filuni  20118  ufilmax  20140  isufil2  20141  cfinufil  20161  fmfnfmlem1  20187  fmfnfmlem2  20188  fmfnfmlem4  20190  fmfnfm  20191  fmco  20194  flimopn  20208  hausflim  20214  flimrest  20216  fclsopn  20247  flimfnfcls  20261  alexsubALTlem2  20280  alexsubALTlem3  20281  alexsubALT  20283  ptcmplem2  20285  cnextcn  20299  symgtgp  20332  divstgplem  20351  tsmsresOLD  20377  tsmsres  20378  tsmsxplem1  20387  isucn2  20514  imasdsf1olem  20608  bldisj  20633  blssps  20659  blss  20660  metcnp3  20775  ngptgp  20882  nrginvrcn  20932  nmoleub  20970  xrsmopn  21049  icccmplem3  21061  reconnlem2  21064  rectbntr0  21069  rescncf  21133  icoopnst  21171  iocopnst  21172  iccpnfcnv  21176  lebnumii  21198  nmoleub2lem  21329  nmhmcn  21335  fgcfil  21442  iscfil3  21444  iscau2  21448  iscau3  21449  iscau4  21450  iscmet3lem2  21463  cfilres  21467  caussi  21468  equivcfil  21470  equivcau  21471  caubl  21478  ivthlem2  21596  ivthlem3  21597  ovoliunlem2  21646  ovoliunnul  21650  ovolicc2lem3  21662  ioombl1lem4  21703  dyadmax  21739  dyadmbl  21741  volsup2  21746  itg2le  21878  itg2const2  21880  itg2seq  21881  itgsplitioo  21976  dvnres  22066  rolle  22123  c1lip1  22130  dvivthlem1  22141  lhop1  22147  dvcnvrelem1  22150  dvfsumrlim  22164  ply1divmo  22268  ig1peu  22304  plypf1  22341  coeaddlem  22377  fta1  22435  quotcan  22436  aalioulem4  22462  ulmcaulem  22520  ulmcn  22525  pilem2  22578  sincosq1lem  22620  sinq12gt0  22630  sinq12ge0  22631  sineq0  22644  tanord1  22654  lognegb  22699  logrec  22876  dcubic  22902  xrlimcnp  23023  o1cxp  23029  ftalem2  23072  ftalem3  23073  fsumdvdscom  23186  chtub  23212  vmasum  23216  bcmono  23277  bposlem3  23286  bposlem7  23290  lgsdir  23330  lgsqrlem2  23342  lgsdchr  23348  lgsquadlem2  23355  2sqlem6  23369  dchrisumlem3  23401  pntrsumbnd2  23477  pntpbnd1  23496  pntibnd  23503  pntlem3  23519  pntleml  23521  brbtwn2  23881  colinearalg  23886  axcontlem10  23949  redwlk  24281  usgra2adedgspthlem2  24285  fargshiftf1  24310  constr3trllem2  24324  4cycl4dv  24340  usg2wlkeq  24381  wwlknred  24396  wwlknextbi  24398  wwlkm1edg  24408  clwlkswlks  24431  clwlkisclwwlklem2fv2  24456  clwlkisclwwlklem2a  24458  clwlkisclwwlklem1  24460  clwwlkf  24467  clwwlkext2edg  24475  wwlksubclwwlk  24477  clwwisshclwwlem1  24478  usg2wotspth  24557  vdusgra0nedg  24581  usgravd0nedg  24591  usgravd00  24592  eupath2  24653  frgraregorufrg  24746  numclwwlkovf2ex  24760  numclwlk1lem2foa  24765  numclwlk1lem2fo  24769  ex-natded5.3-2  24803  isgrpo  24871  opidon  24997  vacn  25277  ubthlem2  25460  htthlem  25507  normgt0  25717  shmodsi  25980  spansneleq  26161  h1datomi  26172  pjjsi  26291  nmcexi  26618  pjnormssi  26760  stm1add3i  26839  golem2  26864  cvnsym  26882  dmdmd  26892  mdslmd1lem1  26917  mdslmd1i  26921  mdexchi  26927  atcveq0  26940  superpos  26946  hatomistici  26954  atoml2i  26975  atcvat2i  26979  chirredlem1  26982  atcvat3i  26988  mdsymlem3  26997  mdsymlem5  26999  cdj3lem2b  27029  cdj3i  27033  supssd  27196  resspos  27306  resstos  27307  submarchi  27389  tpr2rico  27527  ordtrest2NEWlem  27537  xrge0iifcnv  27548  eulerpartlemb  27944  ballotlemfc0  28068  ballotlemfcc  28069  subfacp1lem6  28266  iccllyscon  28332  cvmfolem  28361  cvmliftlem7  28373  cvmliftlem10  28376  ghomf1olem  28506  fprodss  28654  fundmpss  28770  dfon2lem3  28791  dfon2lem6  28794  axext4dist  28807  setlikess  28849  trpredtr  28887  trpredmintr  28888  dftrpred3g  28890  trpredrec  28895  frmin  28896  soseq  28908  wfrlem12  28928  frrlem5e  28969  frrlem11  28973  sltval2  28990  sltres  28998  nodenselem4  29018  nodenselem8  29022  nobndlem6  29031  dfrdg4  29174  5segofs  29230  cgrextend  29232  segconeu  29235  btwncomim  29237  btwnswapid  29241  btwnintr  29243  btwnexch3  29244  btwndiff  29251  ifscgr  29268  cgrxfr  29279  btwnxfr  29280  lineext  29300  brofs2  29301  linecgr  29305  lineid  29307  idinside  29308  endofsegid  29309  btwnconn1lem13  29323  btwnconn3  29327  onsuct0  29480  limsucncmpi  29484  wl-aetr  29557  fin2so  29614  ltflcei  29617  tan2h  29622  heicant  29624  mblfinlem2  29627  mblfinlem3  29628  itg2addnclem  29641  itg2addnclem2  29642  itg2gt0cn  29645  ftc1anclem5  29669  ftc1anclem6  29670  finminlem  29711  nn0prpwlem  29715  cldbnd  29719  clsint2  29722  reftr  29759  fnessref  29763  comppfsc  29777  neibastop3  29781  fgmin  29789  filbcmb  29832  nninfnub  29845  mettrifi  29851  geomcau  29853  istotbnd3  29868  sstotbnd2  29871  ismtybndlem  29903  heibor1lem  29906  heiborlem1  29908  heiborlem8  29915  heiborlem10  29917  heibor  29918  riscer  29992  crngohomfo  30004  keridl  30030  ispridl2  30036  ispridlc  30068  ac6s6  30182  fphpdo  30353  icodiamlt  30358  pellexlem5  30371  pellexlem6  30372  jm2.26lem3  30547  dfac21  30616  unxpwdom3  30645  ordpss  30938  stoweidlem34  31334  ralralimp  31762  zm1nn  31794  ltsubnn0  31796  elfz2z  31800  usgedgimp  31872  usgvincvad  31873  usgedgimpALT  31875  usgvincvadALT  31876  ztprmneprm  32000  lcosslsp  32112  lindslinindsimp1  32131  lindslinindsimp2lem5  32136  snlindsntor  32145  19.41rg  32403  bj-exalimi  33314  lsatcveq0  33829  eqlkr3  33898  atlatmstc  34116  atlrelat1  34118  hlrelat2  34199  intnatN  34203  cvrexchlem  34215  cvratlem  34217  cvrat2  34225  atltcvr  34231  cvrat3  34238  cvrat4  34239  ps-1  34273  ps-2  34274  lplnnle2at  34337  lvolnle3at  34378  2llnma3r  34584  cdlemblem  34589  pmapjoin  34648  elpcliN  34689  lhpmcvr4N  34822  4atexlemnclw  34866  trlnidatb  34973  cdlemc4  34990  cdlemd3  34996  cdleme3g  35030  cdleme7d  35042  cdleme11c  35057  cdleme11dN  35058  cdleme21b  35122  cdleme21c  35123  cdleme21i  35131  cdleme22b  35137  cdleme35fnpq  35245  cdlemf1  35357  trlord  35365  cdlemg6c  35416  dihglblem6  36137  dochlkr  36182  dochkrshp  36183  dihjat1lem  36225  dochexmidlem5  36261  dochexmidlem8  36264