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  6576  tfrlem9  6595  nntri1  6774  nnaordex  6806  ertr  6827  swoord2  6842  findcard2s  7200  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  9767  fzind  9771  fnn0ind  9772  xlesubadd  10301  icoshft  10408  zltaddlt1le  10426  fzen  10463  elfz1b  10513  elfz0fzfz0  10549  elfzmlbp  10555  fzo1fzo0n0  10611  elfzo0z  10612  fzofzim  10616  elfzodifsumelfzo  10635  modqadd1  10818  modqmul1  10834  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  monoord  10942  seqf1oglem1  10976  seqf1oglem2  10977  seq3coll  11315  ccatalpha  11402  swrdsbslen  11459  swrdspsleq  11460  swrdswrdlem  11497  swrdswrd  11498  pfxccatin12lem2a  11520  pfxccatin12lem1  11521  pfxccatin12lem3  11525  swrdccat3blem  11532  reuccatpfxs1lem  11539  caucvgrelemcau  11767  caucvgre  11768  absext  11850  absle  11877  cau3lem  11902  icodiamlt  11968  climuni  12083  mulcn2  12102  cvgratnnlemnexp  12315  cvgratnnlemmn  12316  fprodssdc  12381  p1modz1  12585  dvdsmodexp  12586  dvds2lem  12594  dvdsabseq  12638  bitsinv1lem  12752  dfgcd2  12815  algcvga  12853  coprmgcdb  12890  coprmdvds2  12895  isprm3  12920  prmdvdsfz  12942  coprm  12947  rpexp12i  12958  sqrt2irr  12965  dfphi2  13026  odzdvds  13052  pclemub  13094  pcprendvds  13097  pcpremul  13100  pcqcl  13113  pcdvdsb  13127  pcprmpw2  13140  difsqpwdvds  13145  pcaddlem  13146  pcmptcl  13149  pcfac  13157  prmpwdvds  13162  ballotfilemfc0  13289  ballotfilemfcc  13290  strsetsid  13442  imasabl  14229  lmodfopnelem2  14770  rnglidlmcl  14925  znunit  15102  cncnp  15473  cncnp2m  15474  cnptopresti  15481  lmtopcnp  15493  txcnp  15514  txlm  15522  cnmptcom  15541  bldisj  15644  blssps  15670  blss  15671  metcnp3  15754  rescncf  15824  dedekindeulemloc  15862  dedekindicclemloc  15871  sincosq1lem  16069  sinq12gt0  16074  logbgcd1irr  16220  chtqub  16313  bcmono  16321  bposlem3  16330  bposlem7  16334  lgsdir  16376  gausslemma2dlem6  16408  gausslemma2d  16410  lgsquadlem2  16419  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  2sqlem6  16461  usgruspgrben  16649  subupgr  16736  upgrwlkvtxedg  16827  uspgr2wlkeq  16828  clwwlkext2edg  16885  clwwlknonex2lem2  16901  eupth2lemsfi  16941  bj-sbimedh  17021  decidin  17047  bj-charfunbi  17059  bj-nnelirr  17201