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  2983  trel3  4193  exmidsssnc  4291  poss  4393  sess2  4433  abnexg  4541  funun  5368  ssimaex  5703  f1imass  5910  isores3  5951  isoselem  5956  f1dmex  6273  f1o2ndf1  6388  smoel  6461  tfrlem9  6480  nntri1  6659  nnaordex  6691  ertr  6712  swoord2  6727  findcard2s  7072  pr2ne  7388  addnidpig  7546  ordpipqqs  7584  enq0tr  7644  prloc  7701  addnqprl  7739  addnqpru  7740  mulnqprl  7778  mulnqpru  7779  recexprlemss1l  7845  recexprlemss1u  7846  cauappcvgprlemdisj  7861  mulcmpblnr  7951  ltsrprg  7957  mulextsr1lem  7990  map2psrprg  8015  apreap  8757  mulext1  8782  mulext  8784  mulge0  8789  recexap  8823  lemul12b  9031  mulgt1  9033  lbreu  9115  nnrecgt0  9171  bndndx  9391  uzind  9581  fzind  9585  fnn0ind  9586  xlesubadd  10108  icoshft  10215  zltaddlt1le  10232  fzen  10268  elfz1b  10315  elfz0fzfz0  10351  elfzmlbp  10357  fzo1fzo0n0  10412  elfzo0z  10413  fzofzim  10417  elfzodifsumelfzo  10436  modqadd1  10613  modqmul1  10629  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  monoord  10737  seqf1oglem1  10771  seqf1oglem2  10772  seq3coll  11096  ccatalpha  11180  swrdsbslen  11237  swrdspsleq  11238  swrdswrdlem  11275  swrdswrd  11276  pfxccatin12lem2a  11298  pfxccatin12lem1  11299  pfxccatin12lem3  11303  swrdccat3blem  11310  reuccatpfxs1lem  11317  caucvgrelemcau  11531  caucvgre  11532  absext  11614  absle  11640  cau3lem  11665  icodiamlt  11731  climuni  11844  mulcn2  11863  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  fprodssdc  12141  p1modz1  12345  dvdsmodexp  12346  dvds2lem  12354  dvdsabseq  12398  bitsinv1lem  12512  dfgcd2  12575  algcvga  12613  coprmgcdb  12650  coprmdvds2  12655  isprm3  12680  prmdvdsfz  12701  coprm  12706  rpexp12i  12717  sqrt2irr  12724  dfphi2  12782  odzdvds  12808  pclemub  12850  pcprendvds  12853  pcpremul  12856  pcqcl  12869  pcdvdsb  12883  pcprmpw2  12896  difsqpwdvds  12901  pcaddlem  12902  pcmptcl  12905  pcfac  12913  prmpwdvds  12918  strsetsid  13105  imasabl  13913  lmodfopnelem2  14329  rnglidlmcl  14484  znunit  14663  cncnp  14944  cncnp2m  14945  cnptopresti  14952  lmtopcnp  14964  txcnp  14985  txlm  14993  cnmptcom  15012  bldisj  15115  blssps  15141  blss  15142  metcnp3  15225  rescncf  15295  dedekindeulemloc  15333  dedekindicclemloc  15342  sincosq1lem  15539  sinq12gt0  15544  logbgcd1irr  15681  lgsdir  15754  gausslemma2dlem6  15786  gausslemma2d  15788  lgsquadlem2  15797  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  2sqlem6  15839  usgruspgrben  16025  upgrwlkvtxedg  16161  uspgr2wlkeq  16162  clwwlkext2edg  16217  clwwlknonex2lem2  16233  bj-sbimedh  16303  decidin  16329  bj-charfunbi  16342  bj-nnelirr  16484