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  4151  exmidsssnc  4248  poss  4346  sess2  4386  abnexg  4494  funun  5316  ssimaex  5642  f1imass  5845  isores3  5886  isoselem  5891  f1dmex  6203  f1o2ndf1  6316  smoel  6388  tfrlem9  6407  nntri1  6584  nnaordex  6616  ertr  6637  swoord2  6652  findcard2s  6989  pr2ne  7302  addnidpig  7451  ordpipqqs  7489  enq0tr  7549  prloc  7606  addnqprl  7644  addnqpru  7645  mulnqprl  7683  mulnqpru  7684  recexprlemss1l  7750  recexprlemss1u  7751  cauappcvgprlemdisj  7766  mulcmpblnr  7856  ltsrprg  7862  mulextsr1lem  7895  map2psrprg  7920  apreap  8662  mulext1  8687  mulext  8689  mulge0  8694  recexap  8728  lemul12b  8936  mulgt1  8938  lbreu  9020  nnrecgt0  9076  bndndx  9296  uzind  9486  fzind  9490  fnn0ind  9491  xlesubadd  10007  icoshft  10114  zltaddlt1le  10131  fzen  10167  elfz1b  10214  elfz0fzfz0  10250  elfzmlbp  10256  fzo1fzo0n0  10309  elfzo0z  10310  fzofzim  10314  elfzodifsumelfzo  10332  modqadd1  10508  modqmul1  10524  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  monoord  10632  seqf1oglem1  10666  seqf1oglem2  10667  seq3coll  10989  swrdsbslen  11122  swrdspsleq  11123  caucvgrelemcau  11324  caucvgre  11325  absext  11407  absle  11433  cau3lem  11458  icodiamlt  11524  climuni  11637  mulcn2  11656  cvgratnnlemnexp  11868  cvgratnnlemmn  11869  fprodssdc  11934  p1modz1  12138  dvdsmodexp  12139  dvds2lem  12147  dvdsabseq  12191  bitsinv1lem  12305  dfgcd2  12368  algcvga  12406  coprmgcdb  12443  coprmdvds2  12448  isprm3  12473  prmdvdsfz  12494  coprm  12499  rpexp12i  12510  sqrt2irr  12517  dfphi2  12575  odzdvds  12601  pclemub  12643  pcprendvds  12646  pcpremul  12649  pcqcl  12662  pcdvdsb  12676  pcprmpw2  12689  difsqpwdvds  12694  pcaddlem  12695  pcmptcl  12698  pcfac  12706  prmpwdvds  12711  strsetsid  12898  imasabl  13705  lmodfopnelem2  14120  rnglidlmcl  14275  znunit  14454  cncnp  14735  cncnp2m  14736  cnptopresti  14743  lmtopcnp  14755  txcnp  14776  txlm  14784  cnmptcom  14803  bldisj  14906  blssps  14932  blss  14933  metcnp3  15016  rescncf  15086  dedekindeulemloc  15124  dedekindicclemloc  15133  sincosq1lem  15330  sinq12gt0  15335  logbgcd1irr  15472  lgsdir  15545  gausslemma2dlem6  15577  gausslemma2d  15579  lgsquadlem2  15588  2lgslem3a1  15607  2lgslem3b1  15608  2lgslem3c1  15609  2lgslem3d1  15610  2sqlem6  15630  bj-sbimedh  15744  decidin  15770  bj-charfunbi  15784  bj-nnelirr  15926