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  649  pm5.21ndd  706  mtord  784  pm2.521gdc  869  pm5.11dc  910  anordc  958  hbimd  1584  alrimdd  1620  dral1  1741  sbiedh  1798  ax10oe  1808  sbequi  1850  sbcomxyyz  1988  mo2icl  2939  trel3  4135  exmidsssnc  4232  poss  4329  sess2  4369  abnexg  4477  funun  5298  ssimaex  5618  f1imass  5817  isores3  5858  isoselem  5863  f1dmex  6168  f1o2ndf1  6281  smoel  6353  tfrlem9  6372  nntri1  6549  nnaordex  6581  ertr  6602  swoord2  6617  findcard2s  6946  pr2ne  7252  addnidpig  7396  ordpipqqs  7434  enq0tr  7494  prloc  7551  addnqprl  7589  addnqpru  7590  mulnqprl  7628  mulnqpru  7629  recexprlemss1l  7695  recexprlemss1u  7696  cauappcvgprlemdisj  7711  mulcmpblnr  7801  ltsrprg  7807  mulextsr1lem  7840  map2psrprg  7865  apreap  8606  mulext1  8631  mulext  8633  mulge0  8638  recexap  8672  lemul12b  8880  mulgt1  8882  lbreu  8964  nnrecgt0  9020  bndndx  9239  uzind  9428  fzind  9432  fnn0ind  9433  xlesubadd  9949  icoshft  10056  zltaddlt1le  10073  fzen  10109  elfz1b  10156  elfz0fzfz0  10192  elfzmlbp  10198  fzo1fzo0n0  10250  elfzo0z  10251  fzofzim  10255  elfzodifsumelfzo  10268  modqadd1  10432  modqmul1  10448  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  monoord  10556  seqf1oglem1  10590  seqf1oglem2  10591  seq3coll  10913  caucvgrelemcau  11124  caucvgre  11125  absext  11207  absle  11233  cau3lem  11258  icodiamlt  11324  climuni  11436  mulcn2  11455  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  fprodssdc  11733  p1modz1  11937  dvdsmodexp  11938  dvds2lem  11946  dvdsabseq  11989  dfgcd2  12151  algcvga  12189  coprmgcdb  12226  coprmdvds2  12231  isprm3  12256  prmdvdsfz  12277  coprm  12282  rpexp12i  12293  sqrt2irr  12300  dfphi2  12358  odzdvds  12383  pclemub  12425  pcprendvds  12428  pcpremul  12431  pcqcl  12444  pcdvdsb  12458  pcprmpw2  12471  difsqpwdvds  12476  pcaddlem  12477  pcmptcl  12480  pcfac  12488  prmpwdvds  12493  strsetsid  12651  imasabl  13406  lmodfopnelem2  13821  rnglidlmcl  13976  znunit  14147  cncnp  14398  cncnp2m  14399  cnptopresti  14406  lmtopcnp  14418  txcnp  14439  txlm  14447  cnmptcom  14466  bldisj  14569  blssps  14595  blss  14596  metcnp3  14679  rescncf  14736  dedekindeulemloc  14773  dedekindicclemloc  14782  sincosq1lem  14960  sinq12gt0  14965  logbgcd1irr  15099  lgsdir  15151  gausslemma2dlem6  15183  gausslemma2d  15185  2sqlem6  15207  bj-sbimedh  15263  decidin  15289  bj-charfunbi  15303  bj-nnelirr  15445