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 ) )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syldc  46  3syld  57  sylsyld  58  sylibd  149  sylbid  150  sylibrd  169  sylbird  170  syland  293  animpimp2impd  559  nsyld  651  pm5.21ndd  710  mtord  788  pm2.521gdc  873  pm5.11dc  914  anordc  962  hbimd  1619  alrimdd  1655  dral1  1776  sbiedh  1833  ax10oe  1843  sbequi  1885  sbcomxyyz  2023  mo2icl  2982  trel3  4190  exmidsssnc  4288  poss  4390  sess2  4430  abnexg  4538  funun  5365  ssimaex  5700  f1imass  5907  isores3  5948  isoselem  5953  f1dmex  6270  f1o2ndf1  6385  smoel  6457  tfrlem9  6476  nntri1  6655  nnaordex  6687  ertr  6708  swoord2  6723  findcard2s  7065  pr2ne  7381  addnidpig  7539  ordpipqqs  7577  enq0tr  7637  prloc  7694  addnqprl  7732  addnqpru  7733  mulnqprl  7771  mulnqpru  7772  recexprlemss1l  7838  recexprlemss1u  7839  cauappcvgprlemdisj  7854  mulcmpblnr  7944  ltsrprg  7950  mulextsr1lem  7983  map2psrprg  8008  apreap  8750  mulext1  8775  mulext  8777  mulge0  8782  recexap  8816  lemul12b  9024  mulgt1  9026  lbreu  9108  nnrecgt0  9164  bndndx  9384  uzind  9574  fzind  9578  fnn0ind  9579  xlesubadd  10096  icoshft  10203  zltaddlt1le  10220  fzen  10256  elfz1b  10303  elfz0fzfz0  10339  elfzmlbp  10345  fzo1fzo0n0  10400  elfzo0z  10401  fzofzim  10405  elfzodifsumelfzo  10424  modqadd1  10600  modqmul1  10616  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  monoord  10724  seqf1oglem1  10758  seqf1oglem2  10759  seq3coll  11082  ccatalpha  11166  swrdsbslen  11219  swrdspsleq  11220  swrdswrdlem  11257  swrdswrd  11258  pfxccatin12lem2a  11280  pfxccatin12lem1  11281  pfxccatin12lem3  11285  swrdccat3blem  11292  reuccatpfxs1lem  11299  caucvgrelemcau  11512  caucvgre  11513  absext  11595  absle  11621  cau3lem  11646  icodiamlt  11712  climuni  11825  mulcn2  11844  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  fprodssdc  12122  p1modz1  12326  dvdsmodexp  12327  dvds2lem  12335  dvdsabseq  12379  bitsinv1lem  12493  dfgcd2  12556  algcvga  12594  coprmgcdb  12631  coprmdvds2  12636  isprm3  12661  prmdvdsfz  12682  coprm  12687  rpexp12i  12698  sqrt2irr  12705  dfphi2  12763  odzdvds  12789  pclemub  12831  pcprendvds  12834  pcpremul  12837  pcqcl  12850  pcdvdsb  12864  pcprmpw2  12877  difsqpwdvds  12882  pcaddlem  12883  pcmptcl  12886  pcfac  12894  prmpwdvds  12899  strsetsid  13086  imasabl  13894  lmodfopnelem2  14310  rnglidlmcl  14465  znunit  14644  cncnp  14925  cncnp2m  14926  cnptopresti  14933  lmtopcnp  14945  txcnp  14966  txlm  14974  cnmptcom  14993  bldisj  15096  blssps  15122  blss  15123  metcnp3  15206  rescncf  15276  dedekindeulemloc  15314  dedekindicclemloc  15323  sincosq1lem  15520  sinq12gt0  15525  logbgcd1irr  15662  lgsdir  15735  gausslemma2dlem6  15767  gausslemma2d  15769  lgsquadlem2  15778  2lgslem3a1  15797  2lgslem3b1  15798  2lgslem3c1  15799  2lgslem3d1  15800  2sqlem6  15820  usgruspgrben  16005  upgrwlkvtxedg  16136  uspgr2wlkeq  16137  clwwlkext2edg  16190  bj-sbimedh  16244  decidin  16270  bj-charfunbi  16283  bj-nnelirr  16425