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  4287  poss  4389  sess2  4429  abnexg  4537  funun  5362  ssimaex  5695  f1imass  5898  isores3  5939  isoselem  5944  f1dmex  6261  f1o2ndf1  6374  smoel  6446  tfrlem9  6465  nntri1  6642  nnaordex  6674  ertr  6695  swoord2  6710  findcard2s  7052  pr2ne  7365  addnidpig  7523  ordpipqqs  7561  enq0tr  7621  prloc  7678  addnqprl  7716  addnqpru  7717  mulnqprl  7755  mulnqpru  7756  recexprlemss1l  7822  recexprlemss1u  7823  cauappcvgprlemdisj  7838  mulcmpblnr  7928  ltsrprg  7934  mulextsr1lem  7967  map2psrprg  7992  apreap  8734  mulext1  8759  mulext  8761  mulge0  8766  recexap  8800  lemul12b  9008  mulgt1  9010  lbreu  9092  nnrecgt0  9148  bndndx  9368  uzind  9558  fzind  9562  fnn0ind  9563  xlesubadd  10079  icoshft  10186  zltaddlt1le  10203  fzen  10239  elfz1b  10286  elfz0fzfz0  10322  elfzmlbp  10328  fzo1fzo0n0  10383  elfzo0z  10384  fzofzim  10388  elfzodifsumelfzo  10407  modqadd1  10583  modqmul1  10599  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  monoord  10707  seqf1oglem1  10741  seqf1oglem2  10742  seq3coll  11064  swrdsbslen  11198  swrdspsleq  11199  swrdswrdlem  11236  swrdswrd  11237  pfxccatin12lem2a  11259  pfxccatin12lem1  11260  pfxccatin12lem3  11264  swrdccat3blem  11271  reuccatpfxs1lem  11278  caucvgrelemcau  11491  caucvgre  11492  absext  11574  absle  11600  cau3lem  11625  icodiamlt  11691  climuni  11804  mulcn2  11823  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  fprodssdc  12101  p1modz1  12305  dvdsmodexp  12306  dvds2lem  12314  dvdsabseq  12358  bitsinv1lem  12472  dfgcd2  12535  algcvga  12573  coprmgcdb  12610  coprmdvds2  12615  isprm3  12640  prmdvdsfz  12661  coprm  12666  rpexp12i  12677  sqrt2irr  12684  dfphi2  12742  odzdvds  12768  pclemub  12810  pcprendvds  12813  pcpremul  12816  pcqcl  12829  pcdvdsb  12843  pcprmpw2  12856  difsqpwdvds  12861  pcaddlem  12862  pcmptcl  12865  pcfac  12873  prmpwdvds  12878  strsetsid  13065  imasabl  13873  lmodfopnelem2  14289  rnglidlmcl  14444  znunit  14623  cncnp  14904  cncnp2m  14905  cnptopresti  14912  lmtopcnp  14924  txcnp  14945  txlm  14953  cnmptcom  14972  bldisj  15075  blssps  15101  blss  15102  metcnp3  15185  rescncf  15255  dedekindeulemloc  15293  dedekindicclemloc  15302  sincosq1lem  15499  sinq12gt0  15504  logbgcd1irr  15641  lgsdir  15714  gausslemma2dlem6  15746  gausslemma2d  15748  lgsquadlem2  15757  2lgslem3a1  15776  2lgslem3b1  15777  2lgslem3c1  15778  2lgslem3d1  15779  2sqlem6  15799  usgruspgrben  15984  upgrwlkvtxedg  16075  uspgr2wlkeq  16076  bj-sbimedh  16135  decidin  16161  bj-charfunbi  16174  bj-nnelirr  16316