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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syldc  46  3syld  57  sylsyld  58  sylibd  148  sylbid  149  sylibrd  168  sylbird  169  syland  288  animpimp2impd  527  nsyld  613  pm5.21ndd  657  mtord  733  pm5.11dc  854  anordc  903  hbimd  1511  alrimdd  1546  dral1  1666  sbiedh  1718  ax10oe  1726  sbequi  1768  sbcomxyyz  1895  mo2icl  2795  trel3  3950  poss  4134  sess2  4174  abnexg  4281  funun  5071  ssimaex  5378  f1imass  5567  isores3  5608  isoselem  5613  f1dmex  5901  f1o2ndf1  6007  smoel  6079  tfrlem9  6098  nntri1  6271  nnaordex  6300  ertr  6321  swoord2  6336  findcard2s  6660  pr2ne  6881  addnidpig  6956  ordpipqqs  6994  enq0tr  7054  prloc  7111  addnqprl  7149  addnqpru  7150  mulnqprl  7188  mulnqpru  7189  recexprlemss1l  7255  recexprlemss1u  7256  cauappcvgprlemdisj  7271  mulcmpblnr  7348  ltsrprg  7354  mulextsr1lem  7386  apreap  8125  mulext1  8150  mulext  8152  mulge0  8157  recexap  8183  lemul12b  8383  mulgt1  8385  lbreu  8467  nnrecgt0  8521  bndndx  8733  uzind  8918  fzind  8922  fnn0ind  8923  icoshft  9468  zltaddlt1le  9484  fzen  9518  elfz1b  9565  elfz0fzfz0  9598  elfzmlbp  9604  fzo1fzo0n0  9655  elfzo0z  9656  fzofzim  9660  elfzodifsumelfzo  9673  modqadd1  9829  modqmul1  9845  frecuzrdgtcl  9880  frecuzrdgfunlem  9887  iseqfveq2  9951  iseqshft2  9959  monoord  9965  iseqsplit  9969  iseqid2  10002  iseqcoll  10308  caucvgrelemcau  10474  caucvgre  10475  absext  10557  absle  10583  cau3lem  10608  icodiamlt  10674  climuni  10742  mulcn2  10762  cvgratnnlemnexp  10979  cvgratnnlemmn  10980  dvds2lem  11147  dvdsabseq  11187  dfgcd2  11342  algcvga  11372  coprmgcdb  11409  coprmdvds2  11414  isprm3  11439  prmdvdsfz  11459  coprm  11462  rpexp12i  11473  sqrt2irr  11480  dfphi2  11535  strsetsid  11588  rescncf  11910  bj-sbimedh  11945  decidin  11970  bj-nnelirr  12121