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  548  nsyld  637  pm5.21ndd  694  mtord  772  pm2.521gdc  853  pm5.11dc  894  anordc  940  hbimd  1552  alrimdd  1588  dral1  1708  sbiedh  1760  ax10oe  1769  sbequi  1811  sbcomxyyz  1945  mo2icl  2863  trel3  4034  exmidsssnc  4126  poss  4220  sess2  4260  abnexg  4367  funun  5167  ssimaex  5482  f1imass  5675  isores3  5716  isoselem  5721  f1dmex  6014  f1o2ndf1  6125  smoel  6197  tfrlem9  6216  nntri1  6392  nnaordex  6423  ertr  6444  swoord2  6459  findcard2s  6784  pr2ne  7048  addnidpig  7144  ordpipqqs  7182  enq0tr  7242  prloc  7299  addnqprl  7337  addnqpru  7338  mulnqprl  7376  mulnqpru  7377  recexprlemss1l  7443  recexprlemss1u  7444  cauappcvgprlemdisj  7459  mulcmpblnr  7549  ltsrprg  7555  mulextsr1lem  7588  map2psrprg  7613  apreap  8349  mulext1  8374  mulext  8376  mulge0  8381  recexap  8414  lemul12b  8619  mulgt1  8621  lbreu  8703  nnrecgt0  8758  bndndx  8976  uzind  9162  fzind  9166  fnn0ind  9167  xlesubadd  9666  icoshft  9773  zltaddlt1le  9789  fzen  9823  elfz1b  9870  elfz0fzfz0  9903  elfzmlbp  9909  fzo1fzo0n0  9960  elfzo0z  9961  fzofzim  9965  elfzodifsumelfzo  9978  modqadd1  10134  modqmul1  10150  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  monoord  10249  seq3coll  10585  caucvgrelemcau  10752  caucvgre  10753  absext  10835  absle  10861  cau3lem  10886  icodiamlt  10952  climuni  11062  mulcn2  11081  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  dvds2lem  11505  dvdsabseq  11545  dfgcd2  11702  algcvga  11732  coprmgcdb  11769  coprmdvds2  11774  isprm3  11799  prmdvdsfz  11819  coprm  11822  rpexp12i  11833  sqrt2irr  11840  dfphi2  11896  strsetsid  11992  cncnp  12399  cncnp2m  12400  cnptopresti  12407  lmtopcnp  12419  txcnp  12440  txlm  12448  cnmptcom  12467  bldisj  12570  blssps  12596  blss  12597  metcnp3  12680  rescncf  12737  dedekindeulemloc  12766  dedekindicclemloc  12775  sincosq1lem  12906  sinq12gt0  12911  bj-sbimedh  12978  decidin  13004  bj-nnelirr  13151