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  561  nsyld  653  pm5.21ndd  713  mtord  791  pm2.521gdc  876  pm5.11dc  917  anordc  965  hbimd  1622  alrimdd  1658  dral1  1779  sbiedh  1836  ax10oe  1846  sbequi  1888  sbcomxyyz  2026  mo2icl  2996  trel3  4216  exmidsssnc  4316  poss  4419  sess2  4459  abnexg  4567  funun  5397  ssimaex  5738  f1imass  5947  isores3  5988  isoselem  5993  f1dmex  6309  f1o2ndf1  6424  suppssrst  6461  suppssrgst  6462  smoel  6531  tfrlem9  6550  nntri1  6729  nnaordex  6761  ertr  6782  swoord2  6797  findcard2s  7147  pr2ne  7489  addnidpig  7651  ordpipqqs  7689  enq0tr  7749  prloc  7806  addnqprl  7844  addnqpru  7845  mulnqprl  7883  mulnqpru  7884  recexprlemss1l  7950  recexprlemss1u  7951  cauappcvgprlemdisj  7966  mulcmpblnr  8056  ltsrprg  8062  mulextsr1lem  8095  map2psrprg  8120  apreap  8861  mulext1  8886  mulext  8888  mulge0  8893  recexap  8927  lemul12b  9135  mulgt1  9137  lbreu  9219  nnrecgt0  9275  bndndx  9495  uzind  9689  fzind  9693  fnn0ind  9694  xlesubadd  10216  icoshft  10323  zltaddlt1le  10341  fzen  10377  elfz1b  10424  elfz0fzfz0  10460  elfzmlbp  10466  fzo1fzo0n0  10522  elfzo0z  10523  fzofzim  10527  elfzodifsumelfzo  10546  modqadd1  10723  modqmul1  10739  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  monoord  10847  seqf1oglem1  10881  seqf1oglem2  10882  seq3coll  11214  ccatalpha  11301  swrdsbslen  11358  swrdspsleq  11359  swrdswrdlem  11396  swrdswrd  11397  pfxccatin12lem2a  11419  pfxccatin12lem1  11420  pfxccatin12lem3  11424  swrdccat3blem  11431  reuccatpfxs1lem  11438  caucvgrelemcau  11665  caucvgre  11666  absext  11748  absle  11774  cau3lem  11799  icodiamlt  11865  climuni  11978  mulcn2  11997  cvgratnnlemnexp  12210  cvgratnnlemmn  12211  fprodssdc  12276  p1modz1  12480  dvdsmodexp  12481  dvds2lem  12489  dvdsabseq  12533  bitsinv1lem  12647  dfgcd2  12710  algcvga  12748  coprmgcdb  12785  coprmdvds2  12790  isprm3  12815  prmdvdsfz  12836  coprm  12841  rpexp12i  12852  sqrt2irr  12859  dfphi2  12917  odzdvds  12943  pclemub  12985  pcprendvds  12988  pcpremul  12991  pcqcl  13004  pcdvdsb  13018  pcprmpw2  13031  difsqpwdvds  13036  pcaddlem  13037  pcmptcl  13040  pcfac  13048  prmpwdvds  13053  strsetsid  13245  imasabl  14053  lmodfopnelem2  14473  rnglidlmcl  14628  znunit  14807  cncnp  15095  cncnp2m  15096  cnptopresti  15103  lmtopcnp  15115  txcnp  15136  txlm  15144  cnmptcom  15163  bldisj  15266  blssps  15292  blss  15293  metcnp3  15376  rescncf  15446  dedekindeulemloc  15484  dedekindicclemloc  15493  sincosq1lem  15690  sinq12gt0  15695  logbgcd1irr  15832  lgsdir  15908  gausslemma2dlem6  15940  gausslemma2d  15942  lgsquadlem2  15951  2lgslem3a1  15970  2lgslem3b1  15971  2lgslem3c1  15972  2lgslem3d1  15973  2sqlem6  15993  usgruspgrben  16181  subupgr  16268  upgrwlkvtxedg  16359  uspgr2wlkeq  16360  clwwlkext2edg  16417  clwwlknonex2lem2  16433  eupth2lemsfi  16473  bj-sbimedh  16543  decidin  16569  bj-charfunbi  16581  bj-nnelirr  16723