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  649  pm5.21ndd  707  mtord  785  pm2.521gdc  870  pm5.11dc  911  anordc  959  hbimd  1597  alrimdd  1633  dral1  1754  sbiedh  1811  ax10oe  1821  sbequi  1863  sbcomxyyz  2001  mo2icl  2956  trel3  4158  exmidsssnc  4255  poss  4353  sess2  4393  abnexg  4501  funun  5324  ssimaex  5653  f1imass  5856  isores3  5897  isoselem  5902  f1dmex  6214  f1o2ndf1  6327  smoel  6399  tfrlem9  6418  nntri1  6595  nnaordex  6627  ertr  6648  swoord2  6663  findcard2s  7002  pr2ne  7315  addnidpig  7469  ordpipqqs  7507  enq0tr  7567  prloc  7624  addnqprl  7662  addnqpru  7663  mulnqprl  7701  mulnqpru  7702  recexprlemss1l  7768  recexprlemss1u  7769  cauappcvgprlemdisj  7784  mulcmpblnr  7874  ltsrprg  7880  mulextsr1lem  7913  map2psrprg  7938  apreap  8680  mulext1  8705  mulext  8707  mulge0  8712  recexap  8746  lemul12b  8954  mulgt1  8956  lbreu  9038  nnrecgt0  9094  bndndx  9314  uzind  9504  fzind  9508  fnn0ind  9509  xlesubadd  10025  icoshft  10132  zltaddlt1le  10149  fzen  10185  elfz1b  10232  elfz0fzfz0  10268  elfzmlbp  10274  fzo1fzo0n0  10329  elfzo0z  10330  fzofzim  10334  elfzodifsumelfzo  10352  modqadd1  10528  modqmul1  10544  frecuzrdgtcl  10579  frecuzrdgfunlem  10586  monoord  10652  seqf1oglem1  10686  seqf1oglem2  10687  seq3coll  11009  swrdsbslen  11142  swrdspsleq  11143  swrdswrdlem  11180  swrdswrd  11181  caucvgrelemcau  11366  caucvgre  11367  absext  11449  absle  11475  cau3lem  11500  icodiamlt  11566  climuni  11679  mulcn2  11698  cvgratnnlemnexp  11910  cvgratnnlemmn  11911  fprodssdc  11976  p1modz1  12180  dvdsmodexp  12181  dvds2lem  12189  dvdsabseq  12233  bitsinv1lem  12347  dfgcd2  12410  algcvga  12448  coprmgcdb  12485  coprmdvds2  12490  isprm3  12515  prmdvdsfz  12536  coprm  12541  rpexp12i  12552  sqrt2irr  12559  dfphi2  12617  odzdvds  12643  pclemub  12685  pcprendvds  12688  pcpremul  12691  pcqcl  12704  pcdvdsb  12718  pcprmpw2  12731  difsqpwdvds  12736  pcaddlem  12737  pcmptcl  12740  pcfac  12748  prmpwdvds  12753  strsetsid  12940  imasabl  13747  lmodfopnelem2  14162  rnglidlmcl  14317  znunit  14496  cncnp  14777  cncnp2m  14778  cnptopresti  14785  lmtopcnp  14797  txcnp  14818  txlm  14826  cnmptcom  14845  bldisj  14948  blssps  14974  blss  14975  metcnp3  15058  rescncf  15128  dedekindeulemloc  15166  dedekindicclemloc  15175  sincosq1lem  15372  sinq12gt0  15377  logbgcd1irr  15514  lgsdir  15587  gausslemma2dlem6  15619  gausslemma2d  15621  lgsquadlem2  15630  2lgslem3a1  15649  2lgslem3b1  15650  2lgslem3c1  15651  2lgslem3d1  15652  2sqlem6  15672  bj-sbimedh  15846  decidin  15872  bj-charfunbi  15885  bj-nnelirr  16027