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  649  pm5.21ndd  706  mtord  784  pm2.521gdc  869  pm5.11dc  910  anordc  958  hbimd  1584  alrimdd  1620  dral1  1741  sbiedh  1798  ax10oe  1808  sbequi  1850  sbcomxyyz  1988  mo2icl  2940  trel3  4136  exmidsssnc  4233  poss  4330  sess2  4370  abnexg  4478  funun  5299  ssimaex  5619  f1imass  5818  isores3  5859  isoselem  5864  f1dmex  6170  f1o2ndf1  6283  smoel  6355  tfrlem9  6374  nntri1  6551  nnaordex  6583  ertr  6604  swoord2  6619  findcard2s  6948  pr2ne  7254  addnidpig  7398  ordpipqqs  7436  enq0tr  7496  prloc  7553  addnqprl  7591  addnqpru  7592  mulnqprl  7630  mulnqpru  7631  recexprlemss1l  7697  recexprlemss1u  7698  cauappcvgprlemdisj  7713  mulcmpblnr  7803  ltsrprg  7809  mulextsr1lem  7842  map2psrprg  7867  apreap  8608  mulext1  8633  mulext  8635  mulge0  8640  recexap  8674  lemul12b  8882  mulgt1  8884  lbreu  8966  nnrecgt0  9022  bndndx  9242  uzind  9431  fzind  9435  fnn0ind  9436  xlesubadd  9952  icoshft  10059  zltaddlt1le  10076  fzen  10112  elfz1b  10159  elfz0fzfz0  10195  elfzmlbp  10201  fzo1fzo0n0  10253  elfzo0z  10254  fzofzim  10258  elfzodifsumelfzo  10271  modqadd1  10435  modqmul1  10451  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  monoord  10559  seqf1oglem1  10593  seqf1oglem2  10594  seq3coll  10916  caucvgrelemcau  11127  caucvgre  11128  absext  11210  absle  11236  cau3lem  11261  icodiamlt  11327  climuni  11439  mulcn2  11458  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  fprodssdc  11736  p1modz1  11940  dvdsmodexp  11941  dvds2lem  11949  dvdsabseq  11992  dfgcd2  12154  algcvga  12192  coprmgcdb  12229  coprmdvds2  12234  isprm3  12259  prmdvdsfz  12280  coprm  12285  rpexp12i  12296  sqrt2irr  12303  dfphi2  12361  odzdvds  12386  pclemub  12428  pcprendvds  12431  pcpremul  12434  pcqcl  12447  pcdvdsb  12461  pcprmpw2  12474  difsqpwdvds  12479  pcaddlem  12480  pcmptcl  12483  pcfac  12491  prmpwdvds  12496  strsetsid  12654  imasabl  13409  lmodfopnelem2  13824  rnglidlmcl  13979  znunit  14158  cncnp  14409  cncnp2m  14410  cnptopresti  14417  lmtopcnp  14429  txcnp  14450  txlm  14458  cnmptcom  14477  bldisj  14580  blssps  14606  blss  14607  metcnp3  14690  rescncf  14760  dedekindeulemloc  14798  dedekindicclemloc  14807  sincosq1lem  15001  sinq12gt0  15006  logbgcd1irr  15140  lgsdir  15192  gausslemma2dlem6  15224  gausslemma2d  15226  lgsquadlem2  15235  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  2sqlem6  15277  bj-sbimedh  15333  decidin  15359  bj-charfunbi  15373  bj-nnelirr  15515