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  712  mtord  790  pm2.521gdc  875  pm5.11dc  916  anordc  964  hbimd  1621  alrimdd  1657  dral1  1778  sbiedh  1835  ax10oe  1845  sbequi  1887  sbcomxyyz  2025  mo2icl  2985  trel3  4195  exmidsssnc  4293  poss  4395  sess2  4435  abnexg  4543  funun  5371  ssimaex  5707  f1imass  5915  isores3  5956  isoselem  5961  f1dmex  6278  f1o2ndf1  6393  smoel  6466  tfrlem9  6485  nntri1  6664  nnaordex  6696  ertr  6717  swoord2  6732  findcard2s  7079  pr2ne  7397  addnidpig  7556  ordpipqqs  7594  enq0tr  7654  prloc  7711  addnqprl  7749  addnqpru  7750  mulnqprl  7788  mulnqpru  7789  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemdisj  7871  mulcmpblnr  7961  ltsrprg  7967  mulextsr1lem  8000  map2psrprg  8025  apreap  8767  mulext1  8792  mulext  8794  mulge0  8799  recexap  8833  lemul12b  9041  mulgt1  9043  lbreu  9125  nnrecgt0  9181  bndndx  9401  uzind  9591  fzind  9595  fnn0ind  9596  xlesubadd  10118  icoshft  10225  zltaddlt1le  10242  fzen  10278  elfz1b  10325  elfz0fzfz0  10361  elfzmlbp  10367  fzo1fzo0n0  10423  elfzo0z  10424  fzofzim  10428  elfzodifsumelfzo  10447  modqadd1  10624  modqmul1  10640  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  monoord  10748  seqf1oglem1  10782  seqf1oglem2  10783  seq3coll  11107  ccatalpha  11194  swrdsbslen  11251  swrdspsleq  11252  swrdswrdlem  11289  swrdswrd  11290  pfxccatin12lem2a  11312  pfxccatin12lem1  11313  pfxccatin12lem3  11317  swrdccat3blem  11324  reuccatpfxs1lem  11331  caucvgrelemcau  11558  caucvgre  11559  absext  11641  absle  11667  cau3lem  11692  icodiamlt  11758  climuni  11871  mulcn2  11890  cvgratnnlemnexp  12103  cvgratnnlemmn  12104  fprodssdc  12169  p1modz1  12373  dvdsmodexp  12374  dvds2lem  12382  dvdsabseq  12426  bitsinv1lem  12540  dfgcd2  12603  algcvga  12641  coprmgcdb  12678  coprmdvds2  12683  isprm3  12708  prmdvdsfz  12729  coprm  12734  rpexp12i  12745  sqrt2irr  12752  dfphi2  12810  odzdvds  12836  pclemub  12878  pcprendvds  12881  pcpremul  12884  pcqcl  12897  pcdvdsb  12911  pcprmpw2  12924  difsqpwdvds  12929  pcaddlem  12930  pcmptcl  12933  pcfac  12941  prmpwdvds  12946  strsetsid  13133  imasabl  13941  lmodfopnelem2  14358  rnglidlmcl  14513  znunit  14692  cncnp  14973  cncnp2m  14974  cnptopresti  14981  lmtopcnp  14993  txcnp  15014  txlm  15022  cnmptcom  15041  bldisj  15144  blssps  15170  blss  15171  metcnp3  15254  rescncf  15324  dedekindeulemloc  15362  dedekindicclemloc  15371  sincosq1lem  15568  sinq12gt0  15573  logbgcd1irr  15710  lgsdir  15783  gausslemma2dlem6  15815  gausslemma2d  15817  lgsquadlem2  15826  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgslem3d1  15848  2sqlem6  15868  usgruspgrben  16056  subupgr  16143  upgrwlkvtxedg  16234  uspgr2wlkeq  16235  clwwlkext2edg  16292  clwwlknonex2lem2  16308  eupth2lemsfi  16348  bj-sbimedh  16418  decidin  16444  bj-charfunbi  16457  bj-nnelirr  16599