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  712  mtord  790  pm2.521gdc  875  pm5.11dc  916  anordc  964  hbimd  1621  alrimdd  1657  dral1  1778  sbiedh  1835  ax10oe  1845  sbequi  1887  sbcomxyyz  2025  mo2icl  2985  trel3  4195  exmidsssnc  4293  poss  4395  sess2  4435  abnexg  4543  funun  5371  ssimaex  5707  f1imass  5914  isores3  5955  isoselem  5960  f1dmex  6277  f1o2ndf1  6392  smoel  6465  tfrlem9  6484  nntri1  6663  nnaordex  6695  ertr  6716  swoord2  6731  findcard2s  7078  pr2ne  7396  addnidpig  7555  ordpipqqs  7593  enq0tr  7653  prloc  7710  addnqprl  7748  addnqpru  7749  mulnqprl  7787  mulnqpru  7788  recexprlemss1l  7854  recexprlemss1u  7855  cauappcvgprlemdisj  7870  mulcmpblnr  7960  ltsrprg  7966  mulextsr1lem  7999  map2psrprg  8024  apreap  8766  mulext1  8791  mulext  8793  mulge0  8798  recexap  8832  lemul12b  9040  mulgt1  9042  lbreu  9124  nnrecgt0  9180  bndndx  9400  uzind  9590  fzind  9594  fnn0ind  9595  xlesubadd  10117  icoshft  10224  zltaddlt1le  10241  fzen  10277  elfz1b  10324  elfz0fzfz0  10360  elfzmlbp  10366  fzo1fzo0n0  10421  elfzo0z  10422  fzofzim  10426  elfzodifsumelfzo  10445  modqadd1  10622  modqmul1  10638  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  monoord  10746  seqf1oglem1  10780  seqf1oglem2  10781  seq3coll  11105  ccatalpha  11189  swrdsbslen  11246  swrdspsleq  11247  swrdswrdlem  11284  swrdswrd  11285  pfxccatin12lem2a  11307  pfxccatin12lem1  11308  pfxccatin12lem3  11312  swrdccat3blem  11319  reuccatpfxs1lem  11326  caucvgrelemcau  11540  caucvgre  11541  absext  11623  absle  11649  cau3lem  11674  icodiamlt  11740  climuni  11853  mulcn2  11872  cvgratnnlemnexp  12084  cvgratnnlemmn  12085  fprodssdc  12150  p1modz1  12354  dvdsmodexp  12355  dvds2lem  12363  dvdsabseq  12407  bitsinv1lem  12521  dfgcd2  12584  algcvga  12622  coprmgcdb  12659  coprmdvds2  12664  isprm3  12689  prmdvdsfz  12710  coprm  12715  rpexp12i  12726  sqrt2irr  12733  dfphi2  12791  odzdvds  12817  pclemub  12859  pcprendvds  12862  pcpremul  12865  pcqcl  12878  pcdvdsb  12892  pcprmpw2  12905  difsqpwdvds  12910  pcaddlem  12911  pcmptcl  12914  pcfac  12922  prmpwdvds  12927  strsetsid  13114  imasabl  13922  lmodfopnelem2  14338  rnglidlmcl  14493  znunit  14672  cncnp  14953  cncnp2m  14954  cnptopresti  14961  lmtopcnp  14973  txcnp  14994  txlm  15002  cnmptcom  15021  bldisj  15124  blssps  15150  blss  15151  metcnp3  15234  rescncf  15304  dedekindeulemloc  15342  dedekindicclemloc  15351  sincosq1lem  15548  sinq12gt0  15553  logbgcd1irr  15690  lgsdir  15763  gausslemma2dlem6  15795  gausslemma2d  15797  lgsquadlem2  15806  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  2sqlem6  15848  usgruspgrben  16036  subupgr  16123  upgrwlkvtxedg  16214  uspgr2wlkeq  16215  clwwlkext2edg  16272  clwwlknonex2lem2  16288  bj-sbimedh  16367  decidin  16393  bj-charfunbi  16406  bj-nnelirr  16548