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  7539  addnidpig  7704  ordpipqqs  7742  enq0tr  7802  prloc  7859  addnqprl  7897  addnqpru  7898  mulnqprl  7936  mulnqpru  7937  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemdisj  8019  mulcmpblnr  8109  ltsrprg  8115  mulextsr1lem  8148  map2psrprg  8173  apreap  8918  mulext1  8943  mulext  8945  mulge0  8950  recexap  8984  lemul12b  9194  mulgt1  9196  lbreu  9278  nnrecgt0  9345  bndndx  9567  uzind  9762  fzind  9766  fnn0ind  9767  xlesubadd  10296  icoshft  10403  zltaddlt1le  10421  fzen  10458  elfz1b  10508  elfz0fzfz0  10544  elfzmlbp  10550  fzo1fzo0n0  10606  elfzo0z  10607  fzofzim  10611  elfzodifsumelfzo  10630  modqadd1  10813  modqmul1  10829  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  monoord  10937  seqf1oglem1  10971  seqf1oglem2  10972  seq3coll  11310  ccatalpha  11397  swrdsbslen  11454  swrdspsleq  11455  swrdswrdlem  11492  swrdswrd  11493  pfxccatin12lem2a  11515  pfxccatin12lem1  11516  pfxccatin12lem3  11520  swrdccat3blem  11527  reuccatpfxs1lem  11534  caucvgrelemcau  11762  caucvgre  11763  absext  11845  absle  11872  cau3lem  11897  icodiamlt  11963  climuni  12078  mulcn2  12097  cvgratnnlemnexp  12310  cvgratnnlemmn  12311  fprodssdc  12376  p1modz1  12580  dvdsmodexp  12581  dvds2lem  12589  dvdsabseq  12633  bitsinv1lem  12747  dfgcd2  12810  algcvga  12848  coprmgcdb  12885  coprmdvds2  12890  isprm3  12915  prmdvdsfz  12937  coprm  12942  rpexp12i  12953  sqrt2irr  12960  dfphi2  13021  odzdvds  13047  pclemub  13089  pcprendvds  13092  pcpremul  13095  pcqcl  13108  pcdvdsb  13122  pcprmpw2  13135  difsqpwdvds  13140  pcaddlem  13141  pcmptcl  13144  pcfac  13152  prmpwdvds  13157  ballotfilemfc0  13284  ballotfilemfcc  13285  strsetsid  13437  imasabl  14224  lmodfopnelem2  14753  rnglidlmcl  14908  znunit  15085  cncnp  15430  cncnp2m  15431  cnptopresti  15438  lmtopcnp  15450  txcnp  15471  txlm  15479  cnmptcom  15498  bldisj  15601  blssps  15627  blss  15628  metcnp3  15711  rescncf  15781  dedekindeulemloc  15819  dedekindicclemloc  15828  sincosq1lem  16026  sinq12gt0  16031  logbgcd1irr  16177  chtqub  16270  bcmono  16278  bposlem3  16287  bposlem7  16291  lgsdir  16333  gausslemma2dlem6  16365  gausslemma2d  16367  lgsquadlem2  16376  2lgslem3a1  16395  2lgslem3b1  16396  2lgslem3c1  16397  2lgslem3d1  16398  2sqlem6  16418  usgruspgrben  16606  subupgr  16693  upgrwlkvtxedg  16784  uspgr2wlkeq  16785  clwwlkext2edg  16842  clwwlknonex2lem2  16858  eupth2lemsfi  16898  bj-sbimedh  16978  decidin  17004  bj-charfunbi  17016  bj-nnelirr  17158