Theorem syld 45

Description: Syllogism deduction.

Notice that syld 45 has the same form as syl 14 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 19 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. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)

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

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  syldc  46  3syld  57  sylsyld  58  sylibd  149  sylbid  150  sylibrd  169  sylbird  170  syland  293  animpimp2impd  565  nsyld  657  pm5.21ndd  717  mtord  795  pm2.521gdc  880  pm5.11dc  921  anordc  969  hbimd  1626  alrimdd  1662  dral1  1783  sbiedh  1840  ax10oe  1850  sbequi  1892  sbcomxyyz  2032  mo2icl  3005  trel3  4237  exmidsssnc  4340  poss  4443  sess2  4483  abnexg  4592  funun  5422  ssimaex  5764  f1imass  5980  isores3  6021  isoselem  6026  f1dmex  6345  f1o2ndf1  6464  suppssrst  6501  suppssrgst  6502  smoel  6571  tfrlem9  6590  nntri1  6769  nnaordex  6801  ertr  6822  swoord2  6837  findcard2s  7194  pr2ne  7538  addnidpig  7703  ordpipqqs  7741  enq0tr  7801  prloc  7858  addnqprl  7896  addnqpru  7897  mulnqprl  7935  mulnqpru  7936  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemdisj  8018  mulcmpblnr  8108  ltsrprg  8114  mulextsr1lem  8147  map2psrprg  8172  apreap  8915  mulext1  8940  mulext  8942  mulge0  8947  recexap  8981  lemul12b  9191  mulgt1  9193  lbreu  9275  nnrecgt0  9342  bndndx  9562  uzind  9757  fzind  9761  fnn0ind  9762  xlesubadd  10285  icoshft  10392  zltaddlt1le  10410  fzen  10447  elfz1b  10497  elfz0fzfz0  10533  elfzmlbp  10539  fzo1fzo0n0  10595  elfzo0z  10596  fzofzim  10600  elfzodifsumelfzo  10619  modqadd1  10798  modqmul1  10814  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  monoord  10922  seqf1oglem1  10956  seqf1oglem2  10957  seq3coll  11294  ccatalpha  11381  swrdsbslen  11438  swrdspsleq  11439  swrdswrdlem  11476  swrdswrd  11477  pfxccatin12lem2a  11499  pfxccatin12lem1  11500  pfxccatin12lem3  11504  swrdccat3blem  11511  reuccatpfxs1lem  11518  caucvgrelemcau  11746  caucvgre  11747  absext  11829  absle  11855  cau3lem  11880  icodiamlt  11946  climuni  12059  mulcn2  12078  cvgratnnlemnexp  12291  cvgratnnlemmn  12292  fprodssdc  12357  p1modz1  12561  dvdsmodexp  12562  dvds2lem  12570  dvdsabseq  12614  bitsinv1lem  12728  dfgcd2  12791  algcvga  12829  coprmgcdb  12866  coprmdvds2  12871  isprm3  12896  prmdvdsfz  12917  coprm  12922  rpexp12i  12933  sqrt2irr  12940  dfphi2  12998  odzdvds  13024  pclemub  13066  pcprendvds  13069  pcpremul  13072  pcqcl  13085  pcdvdsb  13099  pcprmpw2  13112  difsqpwdvds  13117  pcaddlem  13118  pcmptcl  13121  pcfac  13129  prmpwdvds  13134  ballotfilemfc0  13232  ballotfilemfcc  13233  strsetsid  13385  imasabl  14140  lmodfopnelem2  14662  rnglidlmcl  14817  znunit  14994  cncnp  15331  cncnp2m  15332  cnptopresti  15339  lmtopcnp  15351  txcnp  15372  txlm  15380  cnmptcom  15399  bldisj  15502  blssps  15528  blss  15529  metcnp3  15612  rescncf  15682  dedekindeulemloc  15720  dedekindicclemloc  15729  sincosq1lem  15926  sinq12gt0  15931  logbgcd1irr  16069  lgsdir  16154  gausslemma2dlem6  16186  gausslemma2d  16188  lgsquadlem2  16197  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  2sqlem6  16239  usgruspgrben  16427  subupgr  16514  upgrwlkvtxedg  16605  uspgr2wlkeq  16606  clwwlkext2edg  16663  clwwlknonex2lem2  16679  eupth2lemsfi  16719  bj-sbimedh  16799  decidin  16825  bj-charfunbi  16837  bj-nnelirr  16979