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  14552  cncnp2m  14553  cnptopresti  14560  lmtopcnp  14572  txcnp  14593  txlm  14601  cnmptcom  14620  bldisj  14723  blssps  14749  blss  14750  metcnp3  14833  rescncf  14903  dedekindeulemloc  14941  dedekindicclemloc  14950  sincosq1lem  15147  sinq12gt0  15152  logbgcd1irr  15289  lgsdir  15362  gausslemma2dlem6  15394  gausslemma2d  15396  lgsquadlem2  15405  2lgslem3a1  15424  2lgslem3b1  15425  2lgslem3c1  15426  2lgslem3d1  15427  2sqlem6  15447  bj-sbimedh  15503  decidin  15529  bj-charfunbi  15543  bj-nnelirr  15685