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  549  nsyld  638  pm5.21ndd  695  mtord  773  pm2.521gdc  854  pm5.11dc  895  anordc  941  hbimd  1553  alrimdd  1589  dral1  1710  sbiedh  1767  ax10oe  1777  sbequi  1819  sbcomxyyz  1952  mo2icl  2891  trel3  4070  exmidsssnc  4163  poss  4257  sess2  4297  abnexg  4404  funun  5211  ssimaex  5526  f1imass  5719  isores3  5760  isoselem  5765  f1dmex  6058  f1o2ndf1  6169  smoel  6241  tfrlem9  6260  nntri1  6436  nnaordex  6467  ertr  6488  swoord2  6503  findcard2s  6828  pr2ne  7110  addnidpig  7239  ordpipqqs  7277  enq0tr  7337  prloc  7394  addnqprl  7432  addnqpru  7433  mulnqprl  7471  mulnqpru  7472  recexprlemss1l  7538  recexprlemss1u  7539  cauappcvgprlemdisj  7554  mulcmpblnr  7644  ltsrprg  7650  mulextsr1lem  7683  map2psrprg  7708  apreap  8445  mulext1  8470  mulext  8472  mulge0  8477  recexap  8510  lemul12b  8715  mulgt1  8717  lbreu  8799  nnrecgt0  8854  bndndx  9072  uzind  9258  fzind  9262  fnn0ind  9263  xlesubadd  9769  icoshft  9876  zltaddlt1le  9893  fzen  9927  elfz1b  9974  elfz0fzfz0  10007  elfzmlbp  10013  fzo1fzo0n0  10064  elfzo0z  10065  fzofzim  10069  elfzodifsumelfzo  10082  modqadd1  10242  modqmul1  10258  frecuzrdgtcl  10293  frecuzrdgfunlem  10300  monoord  10357  seq3coll  10695  caucvgrelemcau  10862  caucvgre  10863  absext  10945  absle  10971  cau3lem  10996  icodiamlt  11062  climuni  11172  mulcn2  11191  cvgratnnlemnexp  11403  cvgratnnlemmn  11404  fprodssdc  11469  p1modz1  11672  dvdsmodexp  11673  dvds2lem  11680  dvdsabseq  11720  dfgcd2  11878  algcvga  11908  coprmgcdb  11945  coprmdvds2  11950  isprm3  11975  prmdvdsfz  11995  coprm  11998  rpexp12i  12009  sqrt2irr  12016  dfphi2  12072  strsetsid  12183  cncnp  12590  cncnp2m  12591  cnptopresti  12598  lmtopcnp  12610  txcnp  12631  txlm  12639  cnmptcom  12658  bldisj  12761  blssps  12787  blss  12788  metcnp3  12871  rescncf  12928  dedekindeulemloc  12957  dedekindicclemloc  12966  sincosq1lem  13106  sinq12gt0  13111  logbgcd1irr  13244  bj-sbimedh  13304  decidin  13330  bj-charfunbi  13345  bj-nnelirr  13487