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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  4239  exmidsssnc  4342  poss  4445  sess2  4485  abnexg  4594  funun  5425  ssimaex  5767  f1imass  5983  isores3  6024  isoselem  6029  f1dmex  6349  f1o2ndf1  6468  suppssrst  6505  suppssrgst  6506  smoel  6575  tfrlem9  6594  nntri1  6773  nnaordex  6805  ertr  6826  swoord2  6841  findcard2s  7198  pr2ne  7544  addnidpig  7709  ordpipqqs  7747  enq0tr  7807  prloc  7864  addnqprl  7902  addnqpru  7903  mulnqprl  7941  mulnqpru  7942  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemdisj  8024  mulcmpblnr  8114  ltsrprg  8120  mulextsr1lem  8153  map2psrprg  8178  apreap  8923  mulext1  8948  mulext  8950  mulge0  8955  recexap  8989  lemul12b  9199  mulgt1  9201  lbreu  9283  nnrecgt0  9351  bndndx  9573  uzind  9768  fzind  9772  fnn0ind  9773  xlesubadd  10302  icoshft  10409  zltaddlt1le  10427  fzen  10464  elfz1b  10514  elfz0fzfz0  10550  elfzmlbp  10556  fzo1fzo0n0  10612  elfzo0z  10613  fzofzim  10617  elfzodifsumelfzo  10636  modqadd1  10819  modqmul1  10835  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  monoord  10943  seqf1oglem1  10977  seqf1oglem2  10978  seq3coll  11316  ccatalpha  11403  swrdsbslen  11460  swrdspsleq  11461  swrdswrdlem  11498  swrdswrd  11499  pfxccatin12lem2a  11521  pfxccatin12lem1  11522  pfxccatin12lem3  11526  swrdccat3blem  11533  reuccatpfxs1lem  11540  caucvgrelemcau  11768  caucvgre  11769  absext  11851  absle  11878  cau3lem  11903  icodiamlt  11969  climuni  12084  mulcn2  12103  cvgratnnlemnexp  12316  cvgratnnlemmn  12317  fprodssdc  12382  p1modz1  12586  dvdsmodexp  12587  dvds2lem  12595  dvdsabseq  12639  bitsinv1lem  12753  dfgcd2  12816  algcvga  12854  coprmgcdb  12891  coprmdvds2  12896  isprm3  12921  prmdvdsfz  12943  coprm  12948  rpexp12i  12959  sqrt2irr  12966  dfphi2  13027  odzdvds  13053  pclemub  13095  pcprendvds  13098  pcpremul  13101  pcqcl  13114  pcdvdsb  13128  pcprmpw2  13141  difsqpwdvds  13146  pcaddlem  13147  pcmptcl  13150  pcfac  13158  prmpwdvds  13163  ballotfilemfc0  13290  ballotfilemfcc  13291  strsetsid  13443  imasabl  14230  lmodfopnelem2  14771  rnglidlmcl  14926  znunit  15103  cncnp  15456  cncnp2m  15457  cnptopresti  15464  lmtopcnp  15476  txcnp  15497  txlm  15505  cnmptcom  15524  bldisj  15627  blssps  15653  blss  15654  metcnp3  15737  rescncf  15807  dedekindeulemloc  15845  dedekindicclemloc  15854  sincosq1lem  16052  sinq12gt0  16057  logbgcd1irr  16203  chtqub  16296  bcmono  16304  bposlem3  16313  bposlem7  16317  lgsdir  16359  gausslemma2dlem6  16391  gausslemma2d  16393  lgsquadlem2  16402  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  2sqlem6  16444  usgruspgrben  16632  subupgr  16719  upgrwlkvtxedg  16810  uspgr2wlkeq  16811  clwwlkext2edg  16868  clwwlknonex2lem2  16884  eupth2lemsfi  16924  bj-sbimedh  17004  decidin  17030  bj-charfunbi  17042  bj-nnelirr  17184