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  4237  exmidsssnc  4340  poss  4443  sess2  4483  abnexg  4592  funun  5422  ssimaex  5764  f1imass  5980  isores3  6021  isoselem  6026  f1dmex  6345  f1o2ndf1  6464  suppssrst  6501  suppssrgst  6502  smoel  6571  tfrlem9  6590  nntri1  6769  nnaordex  6801  ertr  6822  swoord2  6837  findcard2s  7194  pr2ne  7538  addnidpig  7703  ordpipqqs  7741  enq0tr  7801  prloc  7858  addnqprl  7896  addnqpru  7897  mulnqprl  7935  mulnqpru  7936  recexprlemss1l  8002  recexprlemss1u  8003  cauappcvgprlemdisj  8018  mulcmpblnr  8108  ltsrprg  8114  mulextsr1lem  8147  map2psrprg  8172  apreap  8917  mulext1  8942  mulext  8944  mulge0  8949  recexap  8983  lemul12b  9193  mulgt1  9195  lbreu  9277  nnrecgt0  9344  bndndx  9566  uzind  9761  fzind  9765  fnn0ind  9766  xlesubadd  10295  icoshft  10402  zltaddlt1le  10420  fzen  10457  elfz1b  10507  elfz0fzfz0  10543  elfzmlbp  10549  fzo1fzo0n0  10605  elfzo0z  10606  fzofzim  10610  elfzodifsumelfzo  10629  modqadd1  10811  modqmul1  10827  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  monoord  10935  seqf1oglem1  10969  seqf1oglem2  10970  seq3coll  11308  ccatalpha  11395  swrdsbslen  11452  swrdspsleq  11453  swrdswrdlem  11490  swrdswrd  11491  pfxccatin12lem2a  11513  pfxccatin12lem1  11514  pfxccatin12lem3  11518  swrdccat3blem  11525  reuccatpfxs1lem  11532  caucvgrelemcau  11760  caucvgre  11761  absext  11843  absle  11870  cau3lem  11895  icodiamlt  11961  climuni  12075  mulcn2  12094  cvgratnnlemnexp  12307  cvgratnnlemmn  12308  fprodssdc  12373  p1modz1  12577  dvdsmodexp  12578  dvds2lem  12586  dvdsabseq  12630  bitsinv1lem  12744  dfgcd2  12807  algcvga  12845  coprmgcdb  12882  coprmdvds2  12887  isprm3  12912  prmdvdsfz  12934  coprm  12939  rpexp12i  12950  sqrt2irr  12957  dfphi2  13018  odzdvds  13044  pclemub  13086  pcprendvds  13089  pcpremul  13092  pcqcl  13105  pcdvdsb  13119  pcprmpw2  13132  difsqpwdvds  13137  pcaddlem  13138  pcmptcl  13141  pcfac  13149  prmpwdvds  13154  ballotfilemfc0  13281  ballotfilemfcc  13282  strsetsid  13434  imasabl  14189  lmodfopnelem2  14711  rnglidlmcl  14866  znunit  15043  cncnp  15380  cncnp2m  15381  cnptopresti  15388  lmtopcnp  15400  txcnp  15421  txlm  15429  cnmptcom  15448  bldisj  15551  blssps  15577  blss  15578  metcnp3  15661  rescncf  15731  dedekindeulemloc  15769  dedekindicclemloc  15778  sincosq1lem  15976  sinq12gt0  15981  logbgcd1irr  16122  bcmono  16202  bposlem3  16211  lgsdir  16252  gausslemma2dlem6  16284  gausslemma2d  16286  lgsquadlem2  16295  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  2sqlem6  16337  usgruspgrben  16525  subupgr  16612  upgrwlkvtxedg  16703  uspgr2wlkeq  16704  clwwlkext2edg  16761  clwwlknonex2lem2  16777  eupth2lemsfi  16817  bj-sbimedh  16897  decidin  16923  bj-charfunbi  16935  bj-nnelirr  17077