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  148  sylbid  149  sylibrd  168  sylbird  169  syland  291  animpimp2impd  549  nsyld  638  pm5.21ndd  695  mtord  773  pm2.521gdc  854  pm5.11dc  895  anordc  941  hbimd  1553  alrimdd  1589  dral1  1709  sbiedh  1761  ax10oe  1770  sbequi  1812  sbcomxyyz  1946  mo2icl  2867  trel3  4042  exmidsssnc  4134  poss  4228  sess2  4268  abnexg  4375  funun  5175  ssimaex  5490  f1imass  5683  isores3  5724  isoselem  5729  f1dmex  6022  f1o2ndf1  6133  smoel  6205  tfrlem9  6224  nntri1  6400  nnaordex  6431  ertr  6452  swoord2  6467  findcard2s  6792  pr2ne  7065  addnidpig  7168  ordpipqqs  7206  enq0tr  7266  prloc  7323  addnqprl  7361  addnqpru  7362  mulnqprl  7400  mulnqpru  7401  recexprlemss1l  7467  recexprlemss1u  7468  cauappcvgprlemdisj  7483  mulcmpblnr  7573  ltsrprg  7579  mulextsr1lem  7612  map2psrprg  7637  apreap  8373  mulext1  8398  mulext  8400  mulge0  8405  recexap  8438  lemul12b  8643  mulgt1  8645  lbreu  8727  nnrecgt0  8782  bndndx  9000  uzind  9186  fzind  9190  fnn0ind  9191  xlesubadd  9696  icoshft  9803  zltaddlt1le  9820  fzen  9854  elfz1b  9901  elfz0fzfz0  9934  elfzmlbp  9940  fzo1fzo0n0  9991  elfzo0z  9992  fzofzim  9996  elfzodifsumelfzo  10009  modqadd1  10165  modqmul1  10181  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  monoord  10280  seq3coll  10617  caucvgrelemcau  10784  caucvgre  10785  absext  10867  absle  10893  cau3lem  10918  icodiamlt  10984  climuni  11094  mulcn2  11113  cvgratnnlemnexp  11325  cvgratnnlemmn  11326  dvds2lem  11541  dvdsabseq  11581  dfgcd2  11738  algcvga  11768  coprmgcdb  11805  coprmdvds2  11810  isprm3  11835  prmdvdsfz  11855  coprm  11858  rpexp12i  11869  sqrt2irr  11876  dfphi2  11932  strsetsid  12031  cncnp  12438  cncnp2m  12439  cnptopresti  12446  lmtopcnp  12458  txcnp  12479  txlm  12487  cnmptcom  12506  bldisj  12609  blssps  12635  blss  12636  metcnp3  12719  rescncf  12776  dedekindeulemloc  12805  dedekindicclemloc  12814  sincosq1lem  12954  sinq12gt0  12959  logbgcd1irr  13092  bj-sbimedh  13149  decidin  13175  bj-nnelirr  13322