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  148  sylbid  149  sylibrd  168  sylbird  169  syland  291  animpimp2impd  549  nsyld  638  pm5.21ndd  695  mtord  773  pm2.521gdc  858  pm5.11dc  899  anordc  946  hbimd  1561  alrimdd  1597  dral1  1718  sbiedh  1775  ax10oe  1785  sbequi  1827  sbcomxyyz  1960  mo2icl  2905  trel3  4088  exmidsssnc  4182  poss  4276  sess2  4316  abnexg  4424  funun  5232  ssimaex  5547  f1imass  5742  isores3  5783  isoselem  5788  f1dmex  6084  f1o2ndf1  6196  smoel  6268  tfrlem9  6287  nntri1  6464  nnaordex  6495  ertr  6516  swoord2  6531  findcard2s  6856  pr2ne  7148  addnidpig  7277  ordpipqqs  7315  enq0tr  7375  prloc  7432  addnqprl  7470  addnqpru  7471  mulnqprl  7509  mulnqpru  7510  recexprlemss1l  7576  recexprlemss1u  7577  cauappcvgprlemdisj  7592  mulcmpblnr  7682  ltsrprg  7688  mulextsr1lem  7721  map2psrprg  7746  apreap  8485  mulext1  8510  mulext  8512  mulge0  8517  recexap  8550  lemul12b  8756  mulgt1  8758  lbreu  8840  nnrecgt0  8895  bndndx  9113  uzind  9302  fzind  9306  fnn0ind  9307  xlesubadd  9819  icoshft  9926  zltaddlt1le  9943  fzen  9978  elfz1b  10025  elfz0fzfz0  10061  elfzmlbp  10067  fzo1fzo0n0  10118  elfzo0z  10119  fzofzim  10123  elfzodifsumelfzo  10136  modqadd1  10296  modqmul1  10312  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  monoord  10411  seq3coll  10755  caucvgrelemcau  10922  caucvgre  10923  absext  11005  absle  11031  cau3lem  11056  icodiamlt  11122  climuni  11234  mulcn2  11253  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  fprodssdc  11531  p1modz1  11734  dvdsmodexp  11735  dvds2lem  11743  dvdsabseq  11785  dfgcd2  11947  algcvga  11983  coprmgcdb  12020  coprmdvds2  12025  isprm3  12050  prmdvdsfz  12071  coprm  12076  rpexp12i  12087  sqrt2irr  12094  dfphi2  12152  odzdvds  12177  pclemub  12219  pcprendvds  12222  pcpremul  12225  pcqcl  12238  pcdvdsb  12251  pcprmpw2  12264  difsqpwdvds  12269  pcaddlem  12270  pcmptcl  12272  pcfac  12280  prmpwdvds  12285  strsetsid  12427  cncnp  12870  cncnp2m  12871  cnptopresti  12878  lmtopcnp  12890  txcnp  12911  txlm  12919  cnmptcom  12938  bldisj  13041  blssps  13067  blss  13068  metcnp3  13151  rescncf  13208  dedekindeulemloc  13237  dedekindicclemloc  13246  sincosq1lem  13386  sinq12gt0  13391  logbgcd1irr  13525  lgsdir  13576  2sqlem6  13596  bj-sbimedh  13652  decidin  13678  bj-charfunbi  13693  bj-nnelirr  13835