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  707  mtord  785  pm2.521gdc  870  pm5.11dc  911  anordc  959  hbimd  1596  alrimdd  1632  dral1  1753  sbiedh  1810  ax10oe  1820  sbequi  1862  sbcomxyyz  2000  mo2icl  2952  trel3  4150  exmidsssnc  4247  poss  4345  sess2  4385  abnexg  4493  funun  5315  ssimaex  5640  f1imass  5843  isores3  5884  isoselem  5889  f1dmex  6201  f1o2ndf1  6314  smoel  6386  tfrlem9  6405  nntri1  6582  nnaordex  6614  ertr  6635  swoord2  6650  findcard2s  6987  pr2ne  7300  addnidpig  7449  ordpipqqs  7487  enq0tr  7547  prloc  7604  addnqprl  7642  addnqpru  7643  mulnqprl  7681  mulnqpru  7682  recexprlemss1l  7748  recexprlemss1u  7749  cauappcvgprlemdisj  7764  mulcmpblnr  7854  ltsrprg  7860  mulextsr1lem  7893  map2psrprg  7918  apreap  8660  mulext1  8685  mulext  8687  mulge0  8692  recexap  8726  lemul12b  8934  mulgt1  8936  lbreu  9018  nnrecgt0  9074  bndndx  9294  uzind  9484  fzind  9488  fnn0ind  9489  xlesubadd  10005  icoshft  10112  zltaddlt1le  10129  fzen  10165  elfz1b  10212  elfz0fzfz0  10248  elfzmlbp  10254  fzo1fzo0n0  10307  elfzo0z  10308  fzofzim  10312  elfzodifsumelfzo  10330  modqadd1  10506  modqmul1  10522  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  monoord  10630  seqf1oglem1  10664  seqf1oglem2  10665  seq3coll  10987  swrdsbslen  11119  swrdspsleq  11120  caucvgrelemcau  11291  caucvgre  11292  absext  11374  absle  11400  cau3lem  11425  icodiamlt  11491  climuni  11604  mulcn2  11623  cvgratnnlemnexp  11835  cvgratnnlemmn  11836  fprodssdc  11901  p1modz1  12105  dvdsmodexp  12106  dvds2lem  12114  dvdsabseq  12158  bitsinv1lem  12272  dfgcd2  12335  algcvga  12373  coprmgcdb  12410  coprmdvds2  12415  isprm3  12440  prmdvdsfz  12461  coprm  12466  rpexp12i  12477  sqrt2irr  12484  dfphi2  12542  odzdvds  12568  pclemub  12610  pcprendvds  12613  pcpremul  12616  pcqcl  12629  pcdvdsb  12643  pcprmpw2  12656  difsqpwdvds  12661  pcaddlem  12662  pcmptcl  12665  pcfac  12673  prmpwdvds  12678  strsetsid  12865  imasabl  13672  lmodfopnelem2  14087  rnglidlmcl  14242  znunit  14421  cncnp  14702  cncnp2m  14703  cnptopresti  14710  lmtopcnp  14722  txcnp  14743  txlm  14751  cnmptcom  14770  bldisj  14873  blssps  14899  blss  14900  metcnp3  14983  rescncf  15053  dedekindeulemloc  15091  dedekindicclemloc  15100  sincosq1lem  15297  sinq12gt0  15302  logbgcd1irr  15439  lgsdir  15512  gausslemma2dlem6  15544  gausslemma2d  15546  lgsquadlem2  15555  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577  2sqlem6  15597  bj-sbimedh  15711  decidin  15737  bj-charfunbi  15751  bj-nnelirr  15893