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  706  mtord  784  pm2.521gdc  869  pm5.11dc  910  anordc  958  hbimd  1587  alrimdd  1623  dral1  1744  sbiedh  1801  ax10oe  1811  sbequi  1853  sbcomxyyz  1991  mo2icl  2943  trel3  4139  exmidsssnc  4236  poss  4333  sess2  4373  abnexg  4481  funun  5302  ssimaex  5622  f1imass  5821  isores3  5862  isoselem  5867  f1dmex  6173  f1o2ndf1  6286  smoel  6358  tfrlem9  6377  nntri1  6554  nnaordex  6586  ertr  6607  swoord2  6622  findcard2s  6951  pr2ne  7259  addnidpig  7403  ordpipqqs  7441  enq0tr  7501  prloc  7558  addnqprl  7596  addnqpru  7597  mulnqprl  7635  mulnqpru  7636  recexprlemss1l  7702  recexprlemss1u  7703  cauappcvgprlemdisj  7718  mulcmpblnr  7808  ltsrprg  7814  mulextsr1lem  7847  map2psrprg  7872  apreap  8614  mulext1  8639  mulext  8641  mulge0  8646  recexap  8680  lemul12b  8888  mulgt1  8890  lbreu  8972  nnrecgt0  9028  bndndx  9248  uzind  9437  fzind  9441  fnn0ind  9442  xlesubadd  9958  icoshft  10065  zltaddlt1le  10082  fzen  10118  elfz1b  10165  elfz0fzfz0  10201  elfzmlbp  10207  fzo1fzo0n0  10259  elfzo0z  10260  fzofzim  10264  elfzodifsumelfzo  10277  modqadd1  10453  modqmul1  10469  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  monoord  10577  seqf1oglem1  10611  seqf1oglem2  10612  seq3coll  10934  caucvgrelemcau  11145  caucvgre  11146  absext  11228  absle  11254  cau3lem  11279  icodiamlt  11345  climuni  11458  mulcn2  11477  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  fprodssdc  11755  p1modz1  11959  dvdsmodexp  11960  dvds2lem  11968  dvdsabseq  12012  dfgcd2  12181  algcvga  12219  coprmgcdb  12256  coprmdvds2  12261  isprm3  12286  prmdvdsfz  12307  coprm  12312  rpexp12i  12323  sqrt2irr  12330  dfphi2  12388  odzdvds  12414  pclemub  12456  pcprendvds  12459  pcpremul  12462  pcqcl  12475  pcdvdsb  12489  pcprmpw2  12502  difsqpwdvds  12507  pcaddlem  12508  pcmptcl  12511  pcfac  12519  prmpwdvds  12524  strsetsid  12711  imasabl  13466  lmodfopnelem2  13881  rnglidlmcl  14036  znunit  14215  cncnp  14466  cncnp2m  14467  cnptopresti  14474  lmtopcnp  14486  txcnp  14507  txlm  14515  cnmptcom  14534  bldisj  14637  blssps  14663  blss  14664  metcnp3  14747  rescncf  14817  dedekindeulemloc  14855  dedekindicclemloc  14864  sincosq1lem  15061  sinq12gt0  15066  logbgcd1irr  15203  lgsdir  15276  gausslemma2dlem6  15308  gausslemma2d  15310  lgsquadlem2  15319  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  2sqlem6  15361  bj-sbimedh  15417  decidin  15443  bj-charfunbi  15457  bj-nnelirr  15599