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  648  pm5.21ndd  705  mtord  783  pm2.521gdc  868  pm5.11dc  909  anordc  956  hbimd  1573  alrimdd  1609  dral1  1730  sbiedh  1787  ax10oe  1797  sbequi  1839  sbcomxyyz  1972  mo2icl  2917  trel3  4110  exmidsssnc  4204  poss  4299  sess2  4339  abnexg  4447  funun  5261  ssimaex  5578  f1imass  5775  isores3  5816  isoselem  5821  f1dmex  6117  f1o2ndf1  6229  smoel  6301  tfrlem9  6320  nntri1  6497  nnaordex  6529  ertr  6550  swoord2  6565  findcard2s  6890  pr2ne  7191  addnidpig  7335  ordpipqqs  7373  enq0tr  7433  prloc  7490  addnqprl  7528  addnqpru  7529  mulnqprl  7567  mulnqpru  7568  recexprlemss1l  7634  recexprlemss1u  7635  cauappcvgprlemdisj  7650  mulcmpblnr  7740  ltsrprg  7746  mulextsr1lem  7779  map2psrprg  7804  apreap  8544  mulext1  8569  mulext  8571  mulge0  8576  recexap  8610  lemul12b  8818  mulgt1  8820  lbreu  8902  nnrecgt0  8957  bndndx  9175  uzind  9364  fzind  9368  fnn0ind  9369  xlesubadd  9883  icoshft  9990  zltaddlt1le  10007  fzen  10043  elfz1b  10090  elfz0fzfz0  10126  elfzmlbp  10132  fzo1fzo0n0  10183  elfzo0z  10184  fzofzim  10188  elfzodifsumelfzo  10201  modqadd1  10361  modqmul1  10377  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  monoord  10476  seq3coll  10822  caucvgrelemcau  10989  caucvgre  10990  absext  11072  absle  11098  cau3lem  11123  icodiamlt  11189  climuni  11301  mulcn2  11320  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  fprodssdc  11598  p1modz1  11801  dvdsmodexp  11802  dvds2lem  11810  dvdsabseq  11853  dfgcd2  12015  algcvga  12051  coprmgcdb  12088  coprmdvds2  12093  isprm3  12118  prmdvdsfz  12139  coprm  12144  rpexp12i  12155  sqrt2irr  12162  dfphi2  12220  odzdvds  12245  pclemub  12287  pcprendvds  12290  pcpremul  12293  pcqcl  12306  pcdvdsb  12319  pcprmpw2  12332  difsqpwdvds  12337  pcaddlem  12338  pcmptcl  12340  pcfac  12348  prmpwdvds  12353  strsetsid  12495  lmodfopnelem2  13415  cncnp  13733  cncnp2m  13734  cnptopresti  13741  lmtopcnp  13753  txcnp  13774  txlm  13782  cnmptcom  13801  bldisj  13904  blssps  13930  blss  13931  metcnp3  14014  rescncf  14071  dedekindeulemloc  14100  dedekindicclemloc  14109  sincosq1lem  14249  sinq12gt0  14254  logbgcd1irr  14388  lgsdir  14439  2sqlem6  14470  bj-sbimedh  14526  decidin  14552  bj-charfunbi  14566  bj-nnelirr  14708