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  648  pm5.21ndd  705  mtord  783  pm2.521gdc  868  pm5.11dc  909  anordc  956  hbimd  1573  alrimdd  1609  dral1  1730  sbiedh  1787  ax10oe  1797  sbequi  1839  sbcomxyyz  1972  mo2icl  2916  trel3  4109  exmidsssnc  4203  poss  4298  sess2  4338  abnexg  4446  funun  5260  ssimaex  5577  f1imass  5774  isores3  5815  isoselem  5820  f1dmex  6116  f1o2ndf1  6228  smoel  6300  tfrlem9  6319  nntri1  6496  nnaordex  6528  ertr  6549  swoord2  6564  findcard2s  6889  pr2ne  7190  addnidpig  7334  ordpipqqs  7372  enq0tr  7432  prloc  7489  addnqprl  7527  addnqpru  7528  mulnqprl  7566  mulnqpru  7567  recexprlemss1l  7633  recexprlemss1u  7634  cauappcvgprlemdisj  7649  mulcmpblnr  7739  ltsrprg  7745  mulextsr1lem  7778  map2psrprg  7803  apreap  8543  mulext1  8568  mulext  8570  mulge0  8575  recexap  8609  lemul12b  8817  mulgt1  8819  lbreu  8901  nnrecgt0  8956  bndndx  9174  uzind  9363  fzind  9367  fnn0ind  9368  xlesubadd  9882  icoshft  9989  zltaddlt1le  10006  fzen  10042  elfz1b  10089  elfz0fzfz0  10125  elfzmlbp  10131  fzo1fzo0n0  10182  elfzo0z  10183  fzofzim  10187  elfzodifsumelfzo  10200  modqadd1  10360  modqmul1  10376  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  monoord  10475  seq3coll  10821  caucvgrelemcau  10988  caucvgre  10989  absext  11071  absle  11097  cau3lem  11122  icodiamlt  11188  climuni  11300  mulcn2  11319  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  fprodssdc  11597  p1modz1  11800  dvdsmodexp  11801  dvds2lem  11809  dvdsabseq  11852  dfgcd2  12014  algcvga  12050  coprmgcdb  12087  coprmdvds2  12092  isprm3  12117  prmdvdsfz  12138  coprm  12143  rpexp12i  12154  sqrt2irr  12161  dfphi2  12219  odzdvds  12244  pclemub  12286  pcprendvds  12289  pcpremul  12292  pcqcl  12305  pcdvdsb  12318  pcprmpw2  12331  difsqpwdvds  12336  pcaddlem  12337  pcmptcl  12339  pcfac  12347  prmpwdvds  12352  strsetsid  12494  cncnp  13666  cncnp2m  13667  cnptopresti  13674  lmtopcnp  13686  txcnp  13707  txlm  13715  cnmptcom  13734  bldisj  13837  blssps  13863  blss  13864  metcnp3  13947  rescncf  14004  dedekindeulemloc  14033  dedekindicclemloc  14042  sincosq1lem  14182  sinq12gt0  14187  logbgcd1irr  14321  lgsdir  14372  2sqlem6  14403  bj-sbimedh  14459  decidin  14485  bj-charfunbi  14499  bj-nnelirr  14641