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  858  pm5.11dc  899  anordc  946  hbimd  1561  alrimdd  1597  dral1  1718  sbiedh  1775  ax10oe  1785  sbequi  1827  sbcomxyyz  1960  mo2icl  2904  trel3  4087  exmidsssnc  4181  poss  4275  sess2  4315  abnexg  4423  funun  5231  ssimaex  5546  f1imass  5741  isores3  5782  isoselem  5787  f1dmex  6081  f1o2ndf1  6192  smoel  6264  tfrlem9  6283  nntri1  6460  nnaordex  6491  ertr  6512  swoord2  6527  findcard2s  6852  pr2ne  7144  addnidpig  7273  ordpipqqs  7311  enq0tr  7371  prloc  7428  addnqprl  7466  addnqpru  7467  mulnqprl  7505  mulnqpru  7506  recexprlemss1l  7572  recexprlemss1u  7573  cauappcvgprlemdisj  7588  mulcmpblnr  7678  ltsrprg  7684  mulextsr1lem  7717  map2psrprg  7742  apreap  8481  mulext1  8506  mulext  8508  mulge0  8513  recexap  8546  lemul12b  8752  mulgt1  8754  lbreu  8836  nnrecgt0  8891  bndndx  9109  uzind  9298  fzind  9302  fnn0ind  9303  xlesubadd  9815  icoshft  9922  zltaddlt1le  9939  fzen  9974  elfz1b  10021  elfz0fzfz0  10057  elfzmlbp  10063  fzo1fzo0n0  10114  elfzo0z  10115  fzofzim  10119  elfzodifsumelfzo  10132  modqadd1  10292  modqmul1  10308  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  monoord  10407  seq3coll  10751  caucvgrelemcau  10918  caucvgre  10919  absext  11001  absle  11027  cau3lem  11052  icodiamlt  11118  climuni  11230  mulcn2  11249  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  fprodssdc  11527  p1modz1  11730  dvdsmodexp  11731  dvds2lem  11739  dvdsabseq  11781  dfgcd2  11943  algcvga  11979  coprmgcdb  12016  coprmdvds2  12021  isprm3  12046  prmdvdsfz  12067  coprm  12072  rpexp12i  12083  sqrt2irr  12090  dfphi2  12148  odzdvds  12173  pclemub  12215  pcprendvds  12218  pcpremul  12221  pcqcl  12234  pcdvdsb  12247  pcprmpw2  12260  difsqpwdvds  12265  pcaddlem  12266  pcmptcl  12268  pcfac  12276  prmpwdvds  12281  strsetsid  12423  cncnp  12830  cncnp2m  12831  cnptopresti  12838  lmtopcnp  12850  txcnp  12871  txlm  12879  cnmptcom  12898  bldisj  13001  blssps  13027  blss  13028  metcnp3  13111  rescncf  13168  dedekindeulemloc  13197  dedekindicclemloc  13206  sincosq1lem  13346  sinq12gt0  13351  logbgcd1irr  13485  lgsdir  13536  2sqlem6  13556  bj-sbimedh  13612  decidin  13638  bj-charfunbi  13653  bj-nnelirr  13795