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  14746  rnglidlmcl  14901  znunit  15078  cncnp  15422  cncnp2m  15423  cnptopresti  15430  lmtopcnp  15442  txcnp  15463  txlm  15471  cnmptcom  15490  bldisj  15593  blssps  15619  blss  15620  metcnp3  15703  rescncf  15773  dedekindeulemloc  15811  dedekindicclemloc  15820  sincosq1lem  16018  sinq12gt0  16023  logbgcd1irr  16164  chtqub  16257  bcmono  16265  bposlem3  16274  bposlem7  16278  lgsdir  16320  gausslemma2dlem6  16352  gausslemma2d  16354  lgsquadlem2  16363  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  2sqlem6  16405  usgruspgrben  16593  subupgr  16680  upgrwlkvtxedg  16771  uspgr2wlkeq  16772  clwwlkext2edg  16829  clwwlknonex2lem2  16845  eupth2lemsfi  16885  bj-sbimedh  16965  decidin  16991  bj-charfunbi  17003  bj-nnelirr  17145