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  4190  exmidsssnc  4287  poss  4389  sess2  4429  abnexg  4537  funun  5362  ssimaex  5697  f1imass  5904  isores3  5945  isoselem  5950  f1dmex  6267  f1o2ndf1  6380  smoel  6452  tfrlem9  6471  nntri1  6650  nnaordex  6682  ertr  6703  swoord2  6718  findcard2s  7060  pr2ne  7376  addnidpig  7534  ordpipqqs  7572  enq0tr  7632  prloc  7689  addnqprl  7727  addnqpru  7728  mulnqprl  7766  mulnqpru  7767  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemdisj  7849  mulcmpblnr  7939  ltsrprg  7945  mulextsr1lem  7978  map2psrprg  8003  apreap  8745  mulext1  8770  mulext  8772  mulge0  8777  recexap  8811  lemul12b  9019  mulgt1  9021  lbreu  9103  nnrecgt0  9159  bndndx  9379  uzind  9569  fzind  9573  fnn0ind  9574  xlesubadd  10091  icoshft  10198  zltaddlt1le  10215  fzen  10251  elfz1b  10298  elfz0fzfz0  10334  elfzmlbp  10340  fzo1fzo0n0  10395  elfzo0z  10396  fzofzim  10400  elfzodifsumelfzo  10419  modqadd1  10595  modqmul1  10611  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  monoord  10719  seqf1oglem1  10753  seqf1oglem2  10754  seq3coll  11077  ccatalpha  11161  swrdsbslen  11213  swrdspsleq  11214  swrdswrdlem  11251  swrdswrd  11252  pfxccatin12lem2a  11274  pfxccatin12lem1  11275  pfxccatin12lem3  11279  swrdccat3blem  11286  reuccatpfxs1lem  11293  caucvgrelemcau  11506  caucvgre  11507  absext  11589  absle  11615  cau3lem  11640  icodiamlt  11706  climuni  11819  mulcn2  11838  cvgratnnlemnexp  12050  cvgratnnlemmn  12051  fprodssdc  12116  p1modz1  12320  dvdsmodexp  12321  dvds2lem  12329  dvdsabseq  12373  bitsinv1lem  12487  dfgcd2  12550  algcvga  12588  coprmgcdb  12625  coprmdvds2  12630  isprm3  12655  prmdvdsfz  12676  coprm  12681  rpexp12i  12692  sqrt2irr  12699  dfphi2  12757  odzdvds  12783  pclemub  12825  pcprendvds  12828  pcpremul  12831  pcqcl  12844  pcdvdsb  12858  pcprmpw2  12871  difsqpwdvds  12876  pcaddlem  12877  pcmptcl  12880  pcfac  12888  prmpwdvds  12893  strsetsid  13080  imasabl  13888  lmodfopnelem2  14304  rnglidlmcl  14459  znunit  14638  cncnp  14919  cncnp2m  14920  cnptopresti  14927  lmtopcnp  14939  txcnp  14960  txlm  14968  cnmptcom  14987  bldisj  15090  blssps  15116  blss  15117  metcnp3  15200  rescncf  15270  dedekindeulemloc  15308  dedekindicclemloc  15317  sincosq1lem  15514  sinq12gt0  15519  logbgcd1irr  15656  lgsdir  15729  gausslemma2dlem6  15761  gausslemma2d  15763  lgsquadlem2  15772  2lgslem3a1  15791  2lgslem3b1  15792  2lgslem3c1  15793  2lgslem3d1  15794  2sqlem6  15814  usgruspgrben  15999  upgrwlkvtxedg  16105  uspgr2wlkeq  16106  bj-sbimedh  16190  decidin  16216  bj-charfunbi  16229  bj-nnelirr  16371