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  561  nsyld  653  pm5.21ndd  713  mtord  791  pm2.521gdc  876  pm5.11dc  917  anordc  965  hbimd  1622  alrimdd  1658  dral1  1779  sbiedh  1836  ax10oe  1846  sbequi  1888  sbcomxyyz  2028  mo2icl  2999  trel3  4221  exmidsssnc  4321  poss  4424  sess2  4464  abnexg  4572  funun  5402  ssimaex  5743  f1imass  5953  isores3  5994  isoselem  5999  f1dmex  6318  f1o2ndf1  6437  suppssrst  6474  suppssrgst  6475  smoel  6544  tfrlem9  6563  nntri1  6742  nnaordex  6774  ertr  6795  swoord2  6810  findcard2s  7160  pr2ne  7502  addnidpig  7667  ordpipqqs  7705  enq0tr  7765  prloc  7822  addnqprl  7860  addnqpru  7861  mulnqprl  7899  mulnqpru  7900  recexprlemss1l  7966  recexprlemss1u  7967  cauappcvgprlemdisj  7982  mulcmpblnr  8072  ltsrprg  8078  mulextsr1lem  8111  map2psrprg  8136  apreap  8878  mulext1  8903  mulext  8905  mulge0  8910  recexap  8944  lemul12b  9152  mulgt1  9154  lbreu  9236  nnrecgt0  9292  bndndx  9512  uzind  9707  fzind  9711  fnn0ind  9712  xlesubadd  10235  icoshft  10342  zltaddlt1le  10360  fzen  10397  elfz1b  10446  elfz0fzfz0  10482  elfzmlbp  10488  fzo1fzo0n0  10544  elfzo0z  10545  fzofzim  10549  elfzodifsumelfzo  10568  modqadd1  10747  modqmul1  10763  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  monoord  10871  seqf1oglem1  10905  seqf1oglem2  10906  seq3coll  11239  ccatalpha  11326  swrdsbslen  11383  swrdspsleq  11384  swrdswrdlem  11421  swrdswrd  11422  pfxccatin12lem2a  11444  pfxccatin12lem1  11445  pfxccatin12lem3  11449  swrdccat3blem  11456  reuccatpfxs1lem  11463  caucvgrelemcau  11690  caucvgre  11691  absext  11773  absle  11799  cau3lem  11824  icodiamlt  11890  climuni  12003  mulcn2  12022  cvgratnnlemnexp  12235  cvgratnnlemmn  12236  fprodssdc  12301  p1modz1  12505  dvdsmodexp  12506  dvds2lem  12514  dvdsabseq  12558  bitsinv1lem  12672  dfgcd2  12735  algcvga  12773  coprmgcdb  12810  coprmdvds2  12815  isprm3  12840  prmdvdsfz  12861  coprm  12866  rpexp12i  12877  sqrt2irr  12884  dfphi2  12942  odzdvds  12968  pclemub  13010  pcprendvds  13013  pcpremul  13016  pcqcl  13029  pcdvdsb  13043  pcprmpw2  13056  difsqpwdvds  13061  pcaddlem  13062  pcmptcl  13065  pcfac  13073  prmpwdvds  13078  ballotfilemfc0  13176  ballotfilemfcc  13177  strsetsid  13329  imasabl  14089  lmodfopnelem2  14599  rnglidlmcl  14754  znunit  14933  cncnp  15221  cncnp2m  15222  cnptopresti  15229  lmtopcnp  15241  txcnp  15262  txlm  15270  cnmptcom  15289  bldisj  15392  blssps  15418  blss  15419  metcnp3  15502  rescncf  15572  dedekindeulemloc  15610  dedekindicclemloc  15619  sincosq1lem  15816  sinq12gt0  15821  logbgcd1irr  15958  lgsdir  16034  gausslemma2dlem6  16066  gausslemma2d  16068  lgsquadlem2  16077  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  2sqlem6  16119  usgruspgrben  16307  subupgr  16394  upgrwlkvtxedg  16485  uspgr2wlkeq  16486  clwwlkext2edg  16543  clwwlknonex2lem2  16559  eupth2lemsfi  16599  bj-sbimedh  16669  decidin  16695  bj-charfunbi  16707  bj-nnelirr  16849