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  565  nsyld  657  pm5.21ndd  717  mtord  795  pm2.521gdc  880  pm5.11dc  921  anordc  969  hbimd  1626  alrimdd  1662  dral1  1783  sbiedh  1840  ax10oe  1850  sbequi  1892  sbcomxyyz  2032  mo2icl  3005  trel3  4232  exmidsssnc  4335  poss  4438  sess2  4478  abnexg  4587  funun  5417  ssimaex  5758  f1imass  5970  isores3  6011  isoselem  6016  f1dmex  6335  f1o2ndf1  6454  suppssrst  6491  suppssrgst  6492  smoel  6561  tfrlem9  6580  nntri1  6759  nnaordex  6791  ertr  6812  swoord2  6827  findcard2s  7184  pr2ne  7528  addnidpig  7693  ordpipqqs  7731  enq0tr  7791  prloc  7848  addnqprl  7886  addnqpru  7887  mulnqprl  7925  mulnqpru  7926  recexprlemss1l  7992  recexprlemss1u  7993  cauappcvgprlemdisj  8008  mulcmpblnr  8098  ltsrprg  8104  mulextsr1lem  8137  map2psrprg  8162  apreap  8905  mulext1  8930  mulext  8932  mulge0  8937  recexap  8971  lemul12b  9181  mulgt1  9183  lbreu  9265  nnrecgt0  9321  bndndx  9541  uzind  9736  fzind  9740  fnn0ind  9741  xlesubadd  10264  icoshft  10371  zltaddlt1le  10389  fzen  10426  elfz1b  10475  elfz0fzfz0  10511  elfzmlbp  10517  fzo1fzo0n0  10573  elfzo0z  10574  fzofzim  10578  elfzodifsumelfzo  10597  modqadd1  10776  modqmul1  10792  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  monoord  10900  seqf1oglem1  10934  seqf1oglem2  10935  seq3coll  11272  ccatalpha  11359  swrdsbslen  11416  swrdspsleq  11417  swrdswrdlem  11454  swrdswrd  11455  pfxccatin12lem2a  11477  pfxccatin12lem1  11478  pfxccatin12lem3  11482  swrdccat3blem  11489  reuccatpfxs1lem  11496  caucvgrelemcau  11724  caucvgre  11725  absext  11807  absle  11833  cau3lem  11858  icodiamlt  11924  climuni  12037  mulcn2  12056  cvgratnnlemnexp  12269  cvgratnnlemmn  12270  fprodssdc  12335  p1modz1  12539  dvdsmodexp  12540  dvds2lem  12548  dvdsabseq  12592  bitsinv1lem  12706  dfgcd2  12769  algcvga  12807  coprmgcdb  12844  coprmdvds2  12849  isprm3  12874  prmdvdsfz  12895  coprm  12900  rpexp12i  12911  sqrt2irr  12918  dfphi2  12976  odzdvds  13002  pclemub  13044  pcprendvds  13047  pcpremul  13050  pcqcl  13063  pcdvdsb  13077  pcprmpw2  13090  difsqpwdvds  13095  pcaddlem  13096  pcmptcl  13099  pcfac  13107  prmpwdvds  13112  ballotfilemfc0  13210  ballotfilemfcc  13211  strsetsid  13363  imasabl  14117  lmodfopnelem2  14634  rnglidlmcl  14789  znunit  14966  cncnp  15254  cncnp2m  15255  cnptopresti  15262  lmtopcnp  15274  txcnp  15295  txlm  15303  cnmptcom  15322  bldisj  15425  blssps  15451  blss  15452  metcnp3  15535  rescncf  15605  dedekindeulemloc  15643  dedekindicclemloc  15652  sincosq1lem  15849  sinq12gt0  15854  logbgcd1irr  15992  lgsdir  16068  gausslemma2dlem6  16100  gausslemma2d  16102  lgsquadlem2  16111  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  2sqlem6  16153  usgruspgrben  16341  subupgr  16428  upgrwlkvtxedg  16519  uspgr2wlkeq  16520  clwwlkext2edg  16577  clwwlknonex2lem2  16593  eupth2lemsfi  16633  bj-sbimedh  16713  decidin  16739  bj-charfunbi  16751  bj-nnelirr  16893