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  148  sylbid  149  sylibrd  168  sylbird  169  syland  291  animpimp2impd  554  nsyld  643  pm5.21ndd  700  mtord  778  pm2.521gdc  863  pm5.11dc  904  anordc  951  hbimd  1566  alrimdd  1602  dral1  1723  sbiedh  1780  ax10oe  1790  sbequi  1832  sbcomxyyz  1965  mo2icl  2909  trel3  4095  exmidsssnc  4189  poss  4283  sess2  4323  abnexg  4431  funun  5242  ssimaex  5557  f1imass  5753  isores3  5794  isoselem  5799  f1dmex  6095  f1o2ndf1  6207  smoel  6279  tfrlem9  6298  nntri1  6475  nnaordex  6507  ertr  6528  swoord2  6543  findcard2s  6868  pr2ne  7169  addnidpig  7298  ordpipqqs  7336  enq0tr  7396  prloc  7453  addnqprl  7491  addnqpru  7492  mulnqprl  7530  mulnqpru  7531  recexprlemss1l  7597  recexprlemss1u  7598  cauappcvgprlemdisj  7613  mulcmpblnr  7703  ltsrprg  7709  mulextsr1lem  7742  map2psrprg  7767  apreap  8506  mulext1  8531  mulext  8533  mulge0  8538  recexap  8571  lemul12b  8777  mulgt1  8779  lbreu  8861  nnrecgt0  8916  bndndx  9134  uzind  9323  fzind  9327  fnn0ind  9328  xlesubadd  9840  icoshft  9947  zltaddlt1le  9964  fzen  9999  elfz1b  10046  elfz0fzfz0  10082  elfzmlbp  10088  fzo1fzo0n0  10139  elfzo0z  10140  fzofzim  10144  elfzodifsumelfzo  10157  modqadd1  10317  modqmul1  10333  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  monoord  10432  seq3coll  10777  caucvgrelemcau  10944  caucvgre  10945  absext  11027  absle  11053  cau3lem  11078  icodiamlt  11144  climuni  11256  mulcn2  11275  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  fprodssdc  11553  p1modz1  11756  dvdsmodexp  11757  dvds2lem  11765  dvdsabseq  11807  dfgcd2  11969  algcvga  12005  coprmgcdb  12042  coprmdvds2  12047  isprm3  12072  prmdvdsfz  12093  coprm  12098  rpexp12i  12109  sqrt2irr  12116  dfphi2  12174  odzdvds  12199  pclemub  12241  pcprendvds  12244  pcpremul  12247  pcqcl  12260  pcdvdsb  12273  pcprmpw2  12286  difsqpwdvds  12291  pcaddlem  12292  pcmptcl  12294  pcfac  12302  prmpwdvds  12307  strsetsid  12449  cncnp  13024  cncnp2m  13025  cnptopresti  13032  lmtopcnp  13044  txcnp  13065  txlm  13073  cnmptcom  13092  bldisj  13195  blssps  13221  blss  13222  metcnp3  13305  rescncf  13362  dedekindeulemloc  13391  dedekindicclemloc  13400  sincosq1lem  13540  sinq12gt0  13545  logbgcd1irr  13679  lgsdir  13730  2sqlem6  13750  bj-sbimedh  13806  decidin  13832  bj-charfunbi  13846  bj-nnelirr  13988