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  5697  f1imass  5904  isores3  5945  isoselem  5950  f1dmex  6267  f1o2ndf1  6380  smoel  6452  tfrlem9  6471  nntri1  6650  nnaordex  6682  ertr  6703  swoord2  6718  findcard2s  7060  pr2ne  7376  addnidpig  7534  ordpipqqs  7572  enq0tr  7632  prloc  7689  addnqprl  7727  addnqpru  7728  mulnqprl  7766  mulnqpru  7767  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemdisj  7849  mulcmpblnr  7939  ltsrprg  7945  mulextsr1lem  7978  map2psrprg  8003  apreap  8745  mulext1  8770  mulext  8772  mulge0  8777  recexap  8811  lemul12b  9019  mulgt1  9021  lbreu  9103  nnrecgt0  9159  bndndx  9379  uzind  9569  fzind  9573  fnn0ind  9574  xlesubadd  10091  icoshft  10198  zltaddlt1le  10215  fzen  10251  elfz1b  10298  elfz0fzfz0  10334  elfzmlbp  10340  fzo1fzo0n0  10395  elfzo0z  10396  fzofzim  10400  elfzodifsumelfzo  10419  modqadd1  10595  modqmul1  10611  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  monoord  10719  seqf1oglem1  10753  seqf1oglem2  10754  seq3coll  11077  ccatalpha  11161  swrdsbslen  11214  swrdspsleq  11215  swrdswrdlem  11252  swrdswrd  11253  pfxccatin12lem2a  11275  pfxccatin12lem1  11276  pfxccatin12lem3  11280  swrdccat3blem  11287  reuccatpfxs1lem  11294  caucvgrelemcau  11507  caucvgre  11508  absext  11590  absle  11616  cau3lem  11641  icodiamlt  11707  climuni  11820  mulcn2  11839  cvgratnnlemnexp  12051  cvgratnnlemmn  12052  fprodssdc  12117  p1modz1  12321  dvdsmodexp  12322  dvds2lem  12330  dvdsabseq  12374  bitsinv1lem  12488  dfgcd2  12551  algcvga  12589  coprmgcdb  12626  coprmdvds2  12631  isprm3  12656  prmdvdsfz  12677  coprm  12682  rpexp12i  12693  sqrt2irr  12700  dfphi2  12758  odzdvds  12784  pclemub  12826  pcprendvds  12829  pcpremul  12832  pcqcl  12845  pcdvdsb  12859  pcprmpw2  12872  difsqpwdvds  12877  pcaddlem  12878  pcmptcl  12881  pcfac  12889  prmpwdvds  12894  strsetsid  13081  imasabl  13889  lmodfopnelem2  14305  rnglidlmcl  14460  znunit  14639  cncnp  14920  cncnp2m  14921  cnptopresti  14928  lmtopcnp  14940  txcnp  14961  txlm  14969  cnmptcom  14988  bldisj  15091  blssps  15117  blss  15118  metcnp3  15201  rescncf  15271  dedekindeulemloc  15309  dedekindicclemloc  15318  sincosq1lem  15515  sinq12gt0  15520  logbgcd1irr  15657  lgsdir  15730  gausslemma2dlem6  15762  gausslemma2d  15764  lgsquadlem2  15773  2lgslem3a1  15792  2lgslem3b1  15793  2lgslem3c1  15794  2lgslem3d1  15795  2sqlem6  15815  usgruspgrben  16000  upgrwlkvtxedg  16110  uspgr2wlkeq  16111  clwwlkext2edg  16164  bj-sbimedh  16218  decidin  16244  bj-charfunbi  16257  bj-nnelirr  16399