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  1597  alrimdd  1633  dral1  1754  sbiedh  1811  ax10oe  1821  sbequi  1863  sbcomxyyz  2001  mo2icl  2959  trel3  4166  exmidsssnc  4263  poss  4363  sess2  4403  abnexg  4511  funun  5334  ssimaex  5663  f1imass  5866  isores3  5907  isoselem  5912  f1dmex  6224  f1o2ndf1  6337  smoel  6409  tfrlem9  6428  nntri1  6605  nnaordex  6637  ertr  6658  swoord2  6673  findcard2s  7013  pr2ne  7326  addnidpig  7484  ordpipqqs  7522  enq0tr  7582  prloc  7639  addnqprl  7677  addnqpru  7678  mulnqprl  7716  mulnqpru  7717  recexprlemss1l  7783  recexprlemss1u  7784  cauappcvgprlemdisj  7799  mulcmpblnr  7889  ltsrprg  7895  mulextsr1lem  7928  map2psrprg  7953  apreap  8695  mulext1  8720  mulext  8722  mulge0  8727  recexap  8761  lemul12b  8969  mulgt1  8971  lbreu  9053  nnrecgt0  9109  bndndx  9329  uzind  9519  fzind  9523  fnn0ind  9524  xlesubadd  10040  icoshft  10147  zltaddlt1le  10164  fzen  10200  elfz1b  10247  elfz0fzfz0  10283  elfzmlbp  10289  fzo1fzo0n0  10344  elfzo0z  10345  fzofzim  10349  elfzodifsumelfzo  10367  modqadd1  10543  modqmul1  10559  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  monoord  10667  seqf1oglem1  10701  seqf1oglem2  10702  seq3coll  11024  swrdsbslen  11157  swrdspsleq  11158  swrdswrdlem  11195  swrdswrd  11196  pfxccatin12lem2a  11218  pfxccatin12lem1  11219  pfxccatin12lem3  11223  swrdccat3blem  11230  reuccatpfxs1lem  11237  caucvgrelemcau  11406  caucvgre  11407  absext  11489  absle  11515  cau3lem  11540  icodiamlt  11606  climuni  11719  mulcn2  11738  cvgratnnlemnexp  11950  cvgratnnlemmn  11951  fprodssdc  12016  p1modz1  12220  dvdsmodexp  12221  dvds2lem  12229  dvdsabseq  12273  bitsinv1lem  12387  dfgcd2  12450  algcvga  12488  coprmgcdb  12525  coprmdvds2  12530  isprm3  12555  prmdvdsfz  12576  coprm  12581  rpexp12i  12592  sqrt2irr  12599  dfphi2  12657  odzdvds  12683  pclemub  12725  pcprendvds  12728  pcpremul  12731  pcqcl  12744  pcdvdsb  12758  pcprmpw2  12771  difsqpwdvds  12776  pcaddlem  12777  pcmptcl  12780  pcfac  12788  prmpwdvds  12793  strsetsid  12980  imasabl  13787  lmodfopnelem2  14202  rnglidlmcl  14357  znunit  14536  cncnp  14817  cncnp2m  14818  cnptopresti  14825  lmtopcnp  14837  txcnp  14858  txlm  14866  cnmptcom  14885  bldisj  14988  blssps  15014  blss  15015  metcnp3  15098  rescncf  15168  dedekindeulemloc  15206  dedekindicclemloc  15215  sincosq1lem  15412  sinq12gt0  15417  logbgcd1irr  15554  lgsdir  15627  gausslemma2dlem6  15659  gausslemma2d  15661  lgsquadlem2  15670  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgslem3d1  15692  2sqlem6  15712  bj-sbimedh  15907  decidin  15933  bj-charfunbi  15946  bj-nnelirr  16088