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  561  nsyld  653  pm5.21ndd  713  mtord  791  pm2.521gdc  876  pm5.11dc  917  anordc  965  hbimd  1622  alrimdd  1658  dral1  1778  sbiedh  1835  ax10oe  1845  sbequi  1887  sbcomxyyz  2025  mo2icl  2986  trel3  4200  exmidsssnc  4299  poss  4401  sess2  4441  abnexg  4549  funun  5378  ssimaex  5716  f1imass  5925  isores3  5966  isoselem  5971  f1dmex  6287  f1o2ndf1  6402  suppssrst  6439  suppssrgst  6440  smoel  6509  tfrlem9  6528  nntri1  6707  nnaordex  6739  ertr  6760  swoord2  6775  findcard2s  7122  pr2ne  7457  addnidpig  7616  ordpipqqs  7654  enq0tr  7714  prloc  7771  addnqprl  7809  addnqpru  7810  mulnqprl  7848  mulnqpru  7849  recexprlemss1l  7915  recexprlemss1u  7916  cauappcvgprlemdisj  7931  mulcmpblnr  8021  ltsrprg  8027  mulextsr1lem  8060  map2psrprg  8085  apreap  8826  mulext1  8851  mulext  8853  mulge0  8858  recexap  8892  lemul12b  9100  mulgt1  9102  lbreu  9184  nnrecgt0  9240  bndndx  9460  uzind  9652  fzind  9656  fnn0ind  9657  xlesubadd  10179  icoshft  10286  zltaddlt1le  10304  fzen  10340  elfz1b  10387  elfz0fzfz0  10423  elfzmlbp  10429  fzo1fzo0n0  10485  elfzo0z  10486  fzofzim  10490  elfzodifsumelfzo  10509  modqadd1  10686  modqmul1  10702  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  monoord  10810  seqf1oglem1  10844  seqf1oglem2  10845  seq3coll  11169  ccatalpha  11256  swrdsbslen  11313  swrdspsleq  11314  swrdswrdlem  11351  swrdswrd  11352  pfxccatin12lem2a  11374  pfxccatin12lem1  11375  pfxccatin12lem3  11379  swrdccat3blem  11386  reuccatpfxs1lem  11393  caucvgrelemcau  11620  caucvgre  11621  absext  11703  absle  11729  cau3lem  11754  icodiamlt  11820  climuni  11933  mulcn2  11952  cvgratnnlemnexp  12165  cvgratnnlemmn  12166  fprodssdc  12231  p1modz1  12435  dvdsmodexp  12436  dvds2lem  12444  dvdsabseq  12488  bitsinv1lem  12602  dfgcd2  12665  algcvga  12703  coprmgcdb  12740  coprmdvds2  12745  isprm3  12770  prmdvdsfz  12791  coprm  12796  rpexp12i  12807  sqrt2irr  12814  dfphi2  12872  odzdvds  12898  pclemub  12940  pcprendvds  12943  pcpremul  12946  pcqcl  12959  pcdvdsb  12973  pcprmpw2  12986  difsqpwdvds  12991  pcaddlem  12992  pcmptcl  12995  pcfac  13003  prmpwdvds  13008  strsetsid  13195  imasabl  14003  lmodfopnelem2  14421  rnglidlmcl  14576  znunit  14755  cncnp  15041  cncnp2m  15042  cnptopresti  15049  lmtopcnp  15061  txcnp  15082  txlm  15090  cnmptcom  15109  bldisj  15212  blssps  15238  blss  15239  metcnp3  15322  rescncf  15392  dedekindeulemloc  15430  dedekindicclemloc  15439  sincosq1lem  15636  sinq12gt0  15641  logbgcd1irr  15778  lgsdir  15854  gausslemma2dlem6  15886  gausslemma2d  15888  lgsquadlem2  15897  2lgslem3a1  15916  2lgslem3b1  15917  2lgslem3c1  15918  2lgslem3d1  15919  2sqlem6  15939  usgruspgrben  16127  subupgr  16214  upgrwlkvtxedg  16305  uspgr2wlkeq  16306  clwwlkext2edg  16363  clwwlknonex2lem2  16379  eupth2lemsfi  16419  bj-sbimedh  16489  decidin  16515  bj-charfunbi  16527  bj-nnelirr  16669