Theorem syld 40

Description: Syllogism deduction.

Notice that syld 40 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 36	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  3syld  51  sylsyld  52  sylibd  138  sylbid  139  sylibrd  158  sylbird  159  syland  277  nsyld  577  pm5.21ndd  621  mtord  697  pm5.11dc  815  anordc  863  hbimd  1465  alrimdd  1500  dral1  1618  sbiedh  1670  ax10oe  1678  sbequi  1720  sbcomxyyz  1846  mo2icl  2720  trel3  3862  poss  4035  sess2  4075  funun  4944  ssimaex  5234  f1imass  5413  isores3  5455  isoselem  5459  f1dmex  5743  f1o2ndf1  5849  smoel  5915  tfrlem9  5935  nntri1  6074  nnaordex  6100  ertr  6121  swoord2  6136  findcard2s  6347  addnidpig  6434  ordpipqqs  6472  enq0tr  6532  prloc  6589  addnqprl  6627  addnqpru  6628  mulnqprl  6666  mulnqpru  6667  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemdisj  6749  mulcmpblnr  6826  ltsrprg  6832  mulextsr1lem  6864  apreap  7578  mulext1  7603  mulext  7605  mulge0  7610  recexap  7634  lemul12b  7827  mulgt1  7829  nnrecgt0  7951  bndndx  8180  uzind  8349  fzind  8353  fnn0ind  8354  icoshft  8858  fzen  8907  elfz1b  8952  elfz0fzfz0  8983  elfzmlbmOLD  8989  elfzmlbp  8990  fzo1fzo0n0  9039  elfzo0z  9040  fzofzim  9044  elfzodifsumelfzo  9057  frecuzrdgfn  9198  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  caucvgrelemcau  9579  caucvgre  9580  absext  9661  absle  9685  cau3lem  9710  icodiamlt  9776  climuni  9814  mulcn2  9833  sqrt2irr  9878  ialgcvga  9890  bj-sbimedh  9911  bj-nnelirr  10078