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  1814  axc112  1869  cbv1hOLD  1963  nfeqf2  1989  equveliOLD  2039  sbequi  2066  sbiedOLD  2103  dral1-o  2203  ax12indalem  2245  ax12inda2ALT  2246  trel3  4388  poss  4638  sess2  4684  wefrc  4709  wereu2  4712  ordelord  4736  funun  5455  ssimaex  5751  f1imass  5972  soisoi  6014  isores3  6021  isofrlem  6026  isoselem  6027  weniso  6040  oninton  6406  orduniorsuc  6436  limuni3  6458  tfindsg  6466  limom  6486  f1dmex  6542  f1o2ndf1  6675  soxp  6680  extmptsuppeq  6708  smoel  6813  smogt  6820  tfrlem9  6836  tz7.49  6892  seqomlem1  6897  odi  7010  omass  7011  omeulem2  7014  oeordsuc  7025  oeeulem  7032  ertr  7108  swoord2  7123  ecopovtrn  7195  domtriord  7449  2pwuninel  7458  onomeneq  7492  unxpdomlem2  7510  isinf  7518  pssnn  7523  findcard3  7547  frfi  7549  unblem3  7558  dffi3  7673  en3lplem1  7812  inf3lem3  7828  inf3lem5  7830  noinfep  7857  cantnfle  7871  cantnfp1lem3  7880  cantnfleOLD  7901  cantnfp1lem3OLD  7906  rankxpsuc  8081  tcrank  8083  ficardom  8123  carduni  8143  infxpenlem  8172  dfac8alem  8191  ac10ct  8196  ween  8197  alephdom  8243  alephle  8250  iscard3  8255  alephfp  8270  cdainf  8353  pwsdompw  8365  infdif  8370  cfslbn  8428  cofsmo  8430  cfsmolem  8431  cfcof  8435  fin1a2s  8575  domtriomlem  8603  ac6num  8640  zorn2lem3  8659  axdclem2  8681  imadomg  8693  iundom2g  8696  ficard  8721  fpwwe2lem8  8796  fpwwe2  8802  gchaclem  8837  tskr1om2  8927  inar1  8934  tskord  8939  tskuni  8942  grudomon  8976  grur1a  8978  grur1  8979  addnidpi  9062  ltexnq  9136  genpnnp  9166  addclprlem2  9178  mulclprlem  9180  psslinpr  9192  ltaddpr2  9196  ltexprlem6  9202  ltexprlem7  9203  addcanpr  9207  mulgt0sr  9264  map2psrpr  9269  supsrlem  9270  axrrecex  9322  letr  9460  dedekind  9525  recex  9960  lemul12b  10178  mulgt1  10180  ledivmulOLD  10198  fimaxre2  10270  lbreu  10272  nnrecgt0  10351  nnunb  10567  bndndx  10570  zeo  10719  uzind  10725  fzind  10732  fnn0ind  10733  lbzbi  10935  suprzcl2  10937  zmax  10942  rpnnen1lem5  10975  xrletr  11124  qbtwnre  11161  qsqueeze  11163  qextltlem  11164  xralrple  11167  xlesubadd  11218  supxrunb1  11274  icoshft  11399  fzen  11459  elfz0fzfz0  11477  elfzmlbm  11482  elfzmlbp  11483  elfz1b  11519  fzo1fzo0n0  11580  elfzo0z  11581  fzofzim  11585  elfzodifsumelfzo  11596  ssfzoulel  11613  modadd1  11737  modmul1  11744  uzrdgfni  11773  seqcl2  11816  seqfveq2  11820  seqshft2  11824  monoord  11828  seqsplit  11831  seqf1olem1  11837  seqf1olem2  11838  seqid2  11844  seqhomo  11845  expnbnd  11985  faclbnd4lem4  12064  seqcoll  12208  swrdnd  12318  swrdvalodm2  12325  swrdswrdlem  12345  swrdswrd  12346  swrdccatin12lem2a  12368  swrdccatin12lem2b  12369  swrdccatin12lem3  12373  swrdccat3a  12377  swrdccat3blem  12378  repswswrd  12414  swrd2lsw  12544  sqeqd  12647  sqrmo  12733  cau3lem  12834  limsupbnd2  12953  lo1bdd2  12994  climuni  13022  rlimcn2  13060  mulcn2  13065  o1of2  13082  rlimo1  13086  lo1le  13121  isercolllem1  13134  iseralt  13154  isumrpcl  13298  cvgrat  13335  rpnnen2  13500  ruclem3  13507  sqr2irr  13523  dvds2lem  13537  dvdslelem  13569  divalglem8  13596  bitsinv1lem  13629  sadcaddlem  13645  smu01lem  13673  smueqlem  13678  bezoutlem4  13717  algcvga  13746  isprm3  13764  coprm  13778  coprmdvds2  13781  isprm5  13790  rpexp12i  13800  phibndlem  13837  dfphi2  13841  eulerthlem2  13849  odzdvds  13859  iserodd  13894  pclem  13897  pcpremul  13902  pcqcl  13915  pcdvdsb  13927  pcprmpw2  13940  pcaddlem  13942  pcmptcl  13945  pcfac  13953  prmpwdvds  13957  unbenlem  13961  prmreclem1  13969  4sqlem17  14014  vdwmc2  14032  vdwlem9  14042  vdwlem10  14043  vdwlem13  14046  vdwnnlem3  14050  ramcl  14082  mreiincl  14526  pospo  15135  dirge  15399  gsmsymgrfixlem1  15923  oddvdsnn0  16038  oddvds  16041  odcl2  16057  gexdvds  16074  sylow1lem1  16088  sylow2alem2  16108  sylow2a  16109  efgi2  16213  efgsrel  16222  efgs1b  16224  cyggex2  16364  pgpfac1lem2  16564  pgpfac1lem3a  16565  pgpfac1lem3  16566  pgpfac1lem5  16568  lssssr  17011  gzrngunitlem  17852  znunit  17971  frgpcyg  17981  lsmcss  18092  obselocv  18128  obslbs  18130  ordtrest2lem  18782  leordtval2  18791  lecldbas  18798  cncls  18853  cncnp  18859  cnpresti  18867  lmcnp  18883  cnt0  18925  isreg2  18956  cmpsublem  18977  cmpsub  18978  tgcmp  18979  bwth  18988  bwthOLD  18989  dfcon2  18998  1stcfb  19024  2ndcctbss  19034  1stcelcls  19040  islly2  19063  dislly  19076  kgencn2  19105  txcnp  19168  txindis  19182  txcmplem1  19189  txlm  19196  xkohaus  19201  cnmptcom  19226  kqfvima  19278  isr0  19285  fgss2  19422  fbasrn  19432  filuni  19433  ufilmax  19455  isufil2  19456  cfinufil  19476  fmfnfmlem1  19502  fmfnfmlem2  19503  fmfnfmlem4  19505  fmfnfm  19506  fmco  19509  flimopn  19523  hausflim  19529  flimrest  19531  fclsopn  19562  flimfnfcls  19576  alexsubALTlem2  19595  alexsubALTlem3  19596  alexsubALT  19598  ptcmplem2  19600  cnextcn  19614  symgtgp  19647  divstgplem  19666  tsmsresOLD  19692  tsmsres  19693  tsmsxplem1  19702  isucn2  19829  imasdsf1olem  19923  bldisj  19948  blssps  19974  blss  19975  metcnp3  20090  ngptgp  20197  nrginvrcn  20247  nmoleub  20285  xrsmopn  20364  icccmplem3  20376  reconnlem2  20379  rectbntr0  20384  rescncf  20448  icoopnst  20486  iocopnst  20487  iccpnfcnv  20491  lebnumii  20513  nmoleub2lem  20644  nmhmcn  20650  fgcfil  20757  iscfil3  20759  iscau2  20763  iscau3  20764  iscau4  20765  iscmet3lem2  20778  cfilres  20782  caussi  20783  equivcfil  20785  equivcau  20786  caubl  20793  ivthlem2  20911  ivthlem3  20912  ovoliunlem2  20961  ovoliunnul  20965  ovolicc2lem3  20977  ioombl1lem4  21017  dyadmax  21053  dyadmbl  21055  volsup2  21060  itg2le  21192  itg2const2  21194  itg2seq  21195  itgsplitioo  21290  dvnres  21380  rolle  21437  c1lip1  21444  dvivthlem1  21455  lhop1  21461  dvcnvrelem1  21464  dvfsumrlim  21478  ply1divmo  21582  ig1peu  21618  plypf1  21655  coeaddlem  21691  fta1  21749  quotcan  21750  aalioulem4  21776  ulmcaulem  21834  ulmcn  21839  pilem2  21892  sincosq1lem  21934  sinq12gt0  21944  sinq12ge0  21945  sineq0  21958  tanord1  21968  lognegb  22013  logrec  22190  dcubic  22216  xrlimcnp  22337  o1cxp  22343  ftalem2  22386  ftalem3  22387  fsumdvdscom  22500  chtub  22526  vmasum  22530  bcmono  22591  bposlem3  22600  bposlem7  22604  lgsdir  22644  lgsqrlem2  22656  lgsdchr  22662  lgsquadlem2  22669  2sqlem6  22683  dchrisumlem3  22715  pntrsumbnd2  22791  pntpbnd1  22810  pntibnd  22817  pntlem3  22833  pntleml  22835  brbtwn2  23102  colinearalg  23107  axcontlem10  23170  redwlk  23456  fargshiftf1  23474  constr3trllem2  23488  4cycl4dv  23504  vdusgra0nedg  23529  usgravd0nedg  23533  eupath2  23552  ex-natded5.3-2  23566  isgrpo  23634  opidon  23760  vacn  24040  ubthlem2  24223  htthlem  24270  normgt0  24480  shmodsi  24743  spansneleq  24924  h1datomi  24935  pjjsi  25054  nmcexi  25381  pjnormssi  25523  stm1add3i  25602  golem2  25627  cvnsym  25645  dmdmd  25655  mdslmd1lem1  25680  mdslmd1i  25684  mdexchi  25690  atcveq0  25703  superpos  25709  hatomistici  25717  atoml2i  25738  atcvat2i  25742  chirredlem1  25745  atcvat3i  25751  mdsymlem3  25760  mdsymlem5  25762  cdj3lem2b  25792  cdj3i  25796  supssd  25955  resspos  26071  resstos  26072  submarchi  26154  tpr2rico  26294  ordtrest2NEWlem  26304  xrge0iifcnv  26315  eulerpartlemb  26703  ballotlemfc0  26827  ballotlemfcc  26828  subfacp1lem6  27025  iccllyscon  27091  cvmfolem  27120  cvmliftlem7  27132  cvmliftlem10  27135  ghomf1olem  27264  fprodss  27412  fundmpss  27528  dfon2lem3  27549  dfon2lem6  27552  axext4dist  27565  setlikess  27607  trpredtr  27645  trpredmintr  27646  dftrpred3g  27648  trpredrec  27653  frmin  27654  soseq  27666  wfrlem12  27686  frrlem5e  27727  frrlem11  27731  sltval2  27748  sltres  27756  nodenselem4  27776  nodenselem8  27780  nobndlem6  27789  dfrdg4  27932  5segofs  27988  cgrextend  27990  segconeu  27993  btwncomim  27995  btwnswapid  27999  btwnintr  28001  btwnexch3  28002  btwndiff  28009  ifscgr  28026  cgrxfr  28037  btwnxfr  28038  lineext  28058  brofs2  28059  linecgr  28063  lineid  28065  idinside  28066  endofsegid  28067  btwnconn1lem13  28081  btwnconn3  28085  onsuct0  28239  limsucncmpi  28243  wl-aetr  28310  fin2so  28369  ltflcei  28372  tan2h  28377  heicant  28379  mblfinlem2  28382  mblfinlem3  28383  itg2addnclem  28396  itg2addnclem2  28397  itg2gt0cn  28400  ftc1anclem5  28424  ftc1anclem6  28425  finminlem  28466  nn0prpwlem  28470  cldbnd  28474  clsint2  28477  reftr  28514  fnessref  28518  comppfsc  28532  neibastop3  28536  fgmin  28544  filbcmb  28587  nninfnub  28600  mettrifi  28606  geomcau  28608  istotbnd3  28623  sstotbnd2  28626  ismtybndlem  28658  heibor1lem  28661  heiborlem1  28663  heiborlem8  28670  heiborlem10  28672  heibor  28673  riscer  28747  crngohomfo  28759  keridl  28785  ispridl2  28791  ispridlc  28823  ac6s6  28937  fphpdo  29109  icodiamlt  29114  pellexlem5  29127  pellexlem6  29128  jm2.26lem3  29303  dfac21  29372  unxpwdom3  29401  ordpss  29660  stoweidlem34  29782  ralralimp  30072  ltsubnn0  30135  elfz2z  30151  usg2wlkeq  30242  usgra2adedgspthlem2  30257  wwlknred  30308  wwlknextbi  30310  wwlkm1edg  30320  usg2wotspth  30356  clwlkswlks  30376  clwlkisclwwlklem2fv2  30398  clwlkisclwwlklem2a  30400  clwlkisclwwlklem1  30402  clwwlkf  30409  clwwlkext2edg  30417  wwlksubclwwlk  30419  zm1nn  30421  clwwisshclwwlem1  30422  usgravd00  30491  frgraregorufrg  30618  numclwwlkovf2ex  30632  numclwlk1lem2foa  30637  numclwlk1lem2fo  30641  ztprmneprm  30691  suprfinzcl  30696  fsuppmapnn0fiub0  30750  lcosslsp  30861  lindslinindsimp1  30880  lindslinindsimp2lem5  30885  snlindsntor  30894  19.41rg  31146  bj-exalimi  32047  lsatcveq0  32517  eqlkr3  32586  atlatmstc  32804  atlrelat1  32806  hlrelat2  32887  intnatN  32891  cvrexchlem  32903  cvratlem  32905  cvrat2  32913  atltcvr  32919  cvrat3  32926  cvrat4  32927  ps-1  32961  ps-2  32962  lplnnle2at  33025  lvolnle3at  33066  2llnma3r  33272  cdlemblem  33277  pmapjoin  33336  elpcliN  33377  lhpmcvr4N  33510  4atexlemnclw  33554  trlnidatb  33661  cdlemc4  33678  cdlemd3  33684  cdleme3g  33718  cdleme7d  33730  cdleme11c  33745  cdleme11dN  33746  cdleme21b  33810  cdleme21c  33811  cdleme21i  33819  cdleme22b  33825  cdleme35fnpq  33933  cdlemf1  34045  trlord  34053  cdlemg6c  34104  dihglblem6  34825  dochlkr  34870  dochkrshp  34871  dihjat1lem  34913  dochexmidlem5  34949  dochexmidlem8  34952