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  649  pm5.21ndd  706  mtord  784  pm2.521gdc  869  pm5.11dc  910  anordc  958  hbimd  1587  alrimdd  1623  dral1  1744  sbiedh  1801  ax10oe  1811  sbequi  1853  sbcomxyyz  1991  mo2icl  2943  trel3  4140  exmidsssnc  4237  poss  4334  sess2  4374  abnexg  4482  funun  5303  ssimaex  5625  f1imass  5824  isores3  5865  isoselem  5870  f1dmex  6182  f1o2ndf1  6295  smoel  6367  tfrlem9  6386  nntri1  6563  nnaordex  6595  ertr  6616  swoord2  6631  findcard2s  6960  pr2ne  7273  addnidpig  7422  ordpipqqs  7460  enq0tr  7520  prloc  7577  addnqprl  7615  addnqpru  7616  mulnqprl  7654  mulnqpru  7655  recexprlemss1l  7721  recexprlemss1u  7722  cauappcvgprlemdisj  7737  mulcmpblnr  7827  ltsrprg  7833  mulextsr1lem  7866  map2psrprg  7891  apreap  8633  mulext1  8658  mulext  8660  mulge0  8665  recexap  8699  lemul12b  8907  mulgt1  8909  lbreu  8991  nnrecgt0  9047  bndndx  9267  uzind  9456  fzind  9460  fnn0ind  9461  xlesubadd  9977  icoshft  10084  zltaddlt1le  10101  fzen  10137  elfz1b  10184  elfz0fzfz0  10220  elfzmlbp  10226  fzo1fzo0n0  10278  elfzo0z  10279  fzofzim  10283  elfzodifsumelfzo  10296  modqadd1  10472  modqmul1  10488  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  monoord  10596  seqf1oglem1  10630  seqf1oglem2  10631  seq3coll  10953  caucvgrelemcau  11164  caucvgre  11165  absext  11247  absle  11273  cau3lem  11298  icodiamlt  11364  climuni  11477  mulcn2  11496  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  fprodssdc  11774  p1modz1  11978  dvdsmodexp  11979  dvds2lem  11987  dvdsabseq  12031  bitsinv1lem  12145  dfgcd2  12208  algcvga  12246  coprmgcdb  12283  coprmdvds2  12288  isprm3  12313  prmdvdsfz  12334  coprm  12339  rpexp12i  12350  sqrt2irr  12357  dfphi2  12415  odzdvds  12441  pclemub  12483  pcprendvds  12486  pcpremul  12489  pcqcl  12502  pcdvdsb  12516  pcprmpw2  12529  difsqpwdvds  12534  pcaddlem  12535  pcmptcl  12538  pcfac  12546  prmpwdvds  12551  strsetsid  12738  imasabl  13544  lmodfopnelem2  13959  rnglidlmcl  14114  znunit  14293  cncnp  14574  cncnp2m  14575  cnptopresti  14582  lmtopcnp  14594  txcnp  14615  txlm  14623  cnmptcom  14642  bldisj  14745  blssps  14771  blss  14772  metcnp3  14855  rescncf  14925  dedekindeulemloc  14963  dedekindicclemloc  14972  sincosq1lem  15169  sinq12gt0  15174  logbgcd1irr  15311  lgsdir  15384  gausslemma2dlem6  15416  gausslemma2d  15418  lgsquadlem2  15427  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  2sqlem6  15469  bj-sbimedh  15525  decidin  15551  bj-charfunbi  15565  bj-nnelirr  15707