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  610  pm5.21ndd  654  mtord  730  pm5.11dc  851  anordc  900  hbimd  1508  alrimdd  1543  dral1  1662  sbiedh  1714  ax10oe  1722  sbequi  1764  sbcomxyyz  1891  mo2icl  2785  trel3  3921  poss  4101  sess2  4141  funun  5025  ssimaex  5330  f1imass  5516  isores3  5557  isoselem  5562  f1dmex  5846  f1o2ndf1  5952  smoel  6021  tfrlem9  6040  nntri1  6213  nnaordex  6240  ertr  6261  swoord2  6276  findcard2s  6560  pr2ne  6767  addnidpig  6842  ordpipqqs  6880  enq0tr  6940  prloc  6997  addnqprl  7035  addnqpru  7036  mulnqprl  7074  mulnqpru  7075  recexprlemss1l  7141  recexprlemss1u  7142  cauappcvgprlemdisj  7157  mulcmpblnr  7234  ltsrprg  7240  mulextsr1lem  7272  apreap  8008  mulext1  8033  mulext  8035  mulge0  8040  recexap  8064  lemul12b  8260  mulgt1  8262  lbreu  8344  nnrecgt0  8397  bndndx  8608  uzind  8793  fzind  8797  fnn0ind  8798  icoshft  9342  zltaddlt1le  9358  fzen  9392  elfz1b  9437  elfz0fzfz0  9468  elfzmlbp  9474  fzo1fzo0n0  9525  elfzo0z  9526  fzofzim  9530  elfzodifsumelfzo  9543  modqadd1  9699  modqmul1  9715  frecuzrdgtcl  9750  frecuzrdgfunlem  9757  iseqfveq2  9820  iseqshft2  9824  monoord  9829  iseqsplit  9832  iseqid2  9863  iseqcoll  10165  caucvgrelemcau  10330  caucvgre  10331  absext  10413  absle  10439  cau3lem  10464  icodiamlt  10530  climuni  10597  mulcn2  10617  dvds2lem  10733  dvdsabseq  10773  dfgcd2  10928  ialgcvga  10958  coprmgcdb  10995  coprmdvds2  11000  isprm3  11025  prmdvdsfz  11045  coprm  11048  rpexp12i  11059  sqrt2irr  11066  dfphi2  11121  bj-sbimedh  11160  decidin  11185  bj-nnelirr  11336