Theorem syld 45

Description: Syllogism deduction.

Notice that syld 45 has the same form as syl 14 with 𝜑 added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace 𝜑 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	⊢ (𝜑 → (𝜓 → 𝜒))
syld.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
syld	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syld

Step	Hyp	Ref	Expression
1		syld.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syld.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜃))
3	2	a1d 22	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpdd 41	1 ⊢ (𝜑 → (𝜓 → 𝜃))

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  648  pm5.21ndd  705  mtord  783  pm2.521gdc  868  pm5.11dc  909  anordc  956  hbimd  1571  alrimdd  1607  dral1  1728  sbiedh  1785  ax10oe  1795  sbequi  1837  sbcomxyyz  1970  mo2icl  2914  trel3  4104  exmidsssnc  4198  poss  4292  sess2  4332  abnexg  4440  funun  5252  ssimaex  5569  f1imass  5765  isores3  5806  isoselem  5811  f1dmex  6107  f1o2ndf1  6219  smoel  6291  tfrlem9  6310  nntri1  6487  nnaordex  6519  ertr  6540  swoord2  6555  findcard2s  6880  pr2ne  7181  addnidpig  7310  ordpipqqs  7348  enq0tr  7408  prloc  7465  addnqprl  7503  addnqpru  7504  mulnqprl  7542  mulnqpru  7543  recexprlemss1l  7609  recexprlemss1u  7610  cauappcvgprlemdisj  7625  mulcmpblnr  7715  ltsrprg  7721  mulextsr1lem  7754  map2psrprg  7779  apreap  8518  mulext1  8543  mulext  8545  mulge0  8550  recexap  8583  lemul12b  8789  mulgt1  8791  lbreu  8873  nnrecgt0  8928  bndndx  9146  uzind  9335  fzind  9339  fnn0ind  9340  xlesubadd  9852  icoshft  9959  zltaddlt1le  9976  fzen  10011  elfz1b  10058  elfz0fzfz0  10094  elfzmlbp  10100  fzo1fzo0n0  10151  elfzo0z  10152  fzofzim  10156  elfzodifsumelfzo  10169  modqadd1  10329  modqmul1  10345  frecuzrdgtcl  10380  frecuzrdgfunlem  10387  monoord  10444  seq3coll  10788  caucvgrelemcau  10955  caucvgre  10956  absext  11038  absle  11064  cau3lem  11089  icodiamlt  11155  climuni  11267  mulcn2  11286  cvgratnnlemnexp  11498  cvgratnnlemmn  11499  fprodssdc  11564  p1modz1  11767  dvdsmodexp  11768  dvds2lem  11776  dvdsabseq  11818  dfgcd2  11980  algcvga  12016  coprmgcdb  12053  coprmdvds2  12058  isprm3  12083  prmdvdsfz  12104  coprm  12109  rpexp12i  12120  sqrt2irr  12127  dfphi2  12185  odzdvds  12210  pclemub  12252  pcprendvds  12255  pcpremul  12258  pcqcl  12271  pcdvdsb  12284  pcprmpw2  12297  difsqpwdvds  12302  pcaddlem  12303  pcmptcl  12305  pcfac  12313  prmpwdvds  12318  strsetsid  12460  cncnp  13281  cncnp2m  13282  cnptopresti  13289  lmtopcnp  13301  txcnp  13322  txlm  13330  cnmptcom  13349  bldisj  13452  blssps  13478  blss  13479  metcnp3  13562  rescncf  13619  dedekindeulemloc  13648  dedekindicclemloc  13657  sincosq1lem  13797  sinq12gt0  13802  logbgcd1irr  13936  lgsdir  13987  2sqlem6  14007  bj-sbimedh  14063  decidin  14089  bj-charfunbi  14103  bj-nnelirr  14245