Theorem syld 44

Description: Syllogism deduction.

Notice that syld 44 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 40	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:  syldc  45  3syld  56  sylsyld  57  sylibd  147  sylbid  148  sylibrd  167  sylbird  168  syland  287  nsyld  609  pm5.21ndd  653  mtord  729  pm5.11dc  848  anordc  897  hbimd  1505  alrimdd  1540  dral1  1658  sbiedh  1710  ax10oe  1718  sbequi  1760  sbcomxyyz  1887  mo2icl  2771  trel3  3883  poss  4053  sess2  4093  funun  4964  ssimaex  5255  f1imass  5434  isores3  5475  isoselem  5479  f1dmex  5763  f1o2ndf1  5869  smoel  5938  tfrlem9  5958  nntri1  6097  nnaordex  6123  ertr  6144  swoord2  6159  findcard2s  6374  pr2ne  6461  addnidpig  6526  ordpipqqs  6564  enq0tr  6624  prloc  6681  addnqprl  6719  addnqpru  6720  mulnqprl  6758  mulnqpru  6759  recexprlemss1l  6825  recexprlemss1u  6826  cauappcvgprlemdisj  6841  mulcmpblnr  6918  ltsrprg  6924  mulextsr1lem  6956  apreap  7687  mulext1  7712  mulext  7714  mulge0  7719  recexap  7743  lemul12b  7939  mulgt1  7941  lbreu  8023  nnrecgt0  8076  bndndx  8287  uzind  8458  fzind  8462  fnn0ind  8463  icoshft  9012  zltaddlt1le  9028  fzen  9062  elfz1b  9107  elfz0fzfz0  9137  elfzmlbp  9143  fzo1fzo0n0  9192  elfzo0z  9193  fzofzim  9197  elfzodifsumelfzo  9210  modqadd1  9363  modqmul1  9379  frecuzrdgfn  9414  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  caucvgrelemcau  9866  caucvgre  9867  absext  9949  absle  9975  cau3lem  10000  icodiamlt  10066  climuni  10132  mulcn2  10151  dvds2lem  10207  dvdsabseq  10247  dfgcd2  10403  ialgcvga  10433  coprmgcdb  10470  coprmdvds2  10475  isprm3  10500  prmdvdsfz  10520  coprm  10523  rpexp12i  10534  sqrt2irr  10541  bj-sbimedh  10582  bj-nnelirr  10748