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  559  nsyld  651  pm5.21ndd  710  mtord  788  pm2.521gdc  873  pm5.11dc  914  anordc  962  hbimd  1619  alrimdd  1655  dral1  1776  sbiedh  1833  ax10oe  1843  sbequi  1885  sbcomxyyz  2023  mo2icl  2982  trel3  4189  exmidsssnc  4286  poss  4388  sess2  4428  abnexg  4536  funun  5361  ssimaex  5694  f1imass  5897  isores3  5938  isoselem  5943  f1dmex  6259  f1o2ndf1  6372  smoel  6444  tfrlem9  6463  nntri1  6640  nnaordex  6672  ertr  6693  swoord2  6708  findcard2s  7048  pr2ne  7361  addnidpig  7519  ordpipqqs  7557  enq0tr  7617  prloc  7674  addnqprl  7712  addnqpru  7713  mulnqprl  7751  mulnqpru  7752  recexprlemss1l  7818  recexprlemss1u  7819  cauappcvgprlemdisj  7834  mulcmpblnr  7924  ltsrprg  7930  mulextsr1lem  7963  map2psrprg  7988  apreap  8730  mulext1  8755  mulext  8757  mulge0  8762  recexap  8796  lemul12b  9004  mulgt1  9006  lbreu  9088  nnrecgt0  9144  bndndx  9364  uzind  9554  fzind  9558  fnn0ind  9559  xlesubadd  10075  icoshft  10182  zltaddlt1le  10199  fzen  10235  elfz1b  10282  elfz0fzfz0  10318  elfzmlbp  10324  fzo1fzo0n0  10379  elfzo0z  10380  fzofzim  10384  elfzodifsumelfzo  10402  modqadd1  10578  modqmul1  10594  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  monoord  10702  seqf1oglem1  10736  seqf1oglem2  10737  seq3coll  11059  swrdsbslen  11193  swrdspsleq  11194  swrdswrdlem  11231  swrdswrd  11232  pfxccatin12lem2a  11254  pfxccatin12lem1  11255  pfxccatin12lem3  11259  swrdccat3blem  11266  reuccatpfxs1lem  11273  caucvgrelemcau  11486  caucvgre  11487  absext  11569  absle  11595  cau3lem  11620  icodiamlt  11686  climuni  11799  mulcn2  11818  cvgratnnlemnexp  12030  cvgratnnlemmn  12031  fprodssdc  12096  p1modz1  12300  dvdsmodexp  12301  dvds2lem  12309  dvdsabseq  12353  bitsinv1lem  12467  dfgcd2  12530  algcvga  12568  coprmgcdb  12605  coprmdvds2  12610  isprm3  12635  prmdvdsfz  12656  coprm  12661  rpexp12i  12672  sqrt2irr  12679  dfphi2  12737  odzdvds  12763  pclemub  12805  pcprendvds  12808  pcpremul  12811  pcqcl  12824  pcdvdsb  12838  pcprmpw2  12851  difsqpwdvds  12856  pcaddlem  12857  pcmptcl  12860  pcfac  12868  prmpwdvds  12873  strsetsid  13060  imasabl  13868  lmodfopnelem2  14283  rnglidlmcl  14438  znunit  14617  cncnp  14898  cncnp2m  14899  cnptopresti  14906  lmtopcnp  14918  txcnp  14939  txlm  14947  cnmptcom  14966  bldisj  15069  blssps  15095  blss  15096  metcnp3  15179  rescncf  15249  dedekindeulemloc  15287  dedekindicclemloc  15296  sincosq1lem  15493  sinq12gt0  15498  logbgcd1irr  15635  lgsdir  15708  gausslemma2dlem6  15740  gausslemma2d  15742  lgsquadlem2  15751  2lgslem3a1  15770  2lgslem3b1  15771  2lgslem3c1  15772  2lgslem3d1  15773  2sqlem6  15793  usgruspgrben  15978  bj-sbimedh  16093  decidin  16119  bj-charfunbi  16132  bj-nnelirr  16274