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  548  nsyld  637  pm5.21ndd  694  mtord  772  pm2.521gdc  853  pm5.11dc  894  anordc  940  hbimd  1552  alrimdd  1588  dral1  1708  sbiedh  1760  ax10oe  1769  sbequi  1811  sbcomxyyz  1943  mo2icl  2858  trel3  4029  exmidsssnc  4121  poss  4215  sess2  4255  abnexg  4362  funun  5162  ssimaex  5475  f1imass  5668  isores3  5709  isoselem  5714  f1dmex  6007  f1o2ndf1  6118  smoel  6190  tfrlem9  6209  nntri1  6385  nnaordex  6416  ertr  6437  swoord2  6452  findcard2s  6777  pr2ne  7041  addnidpig  7137  ordpipqqs  7175  enq0tr  7235  prloc  7292  addnqprl  7330  addnqpru  7331  mulnqprl  7369  mulnqpru  7370  recexprlemss1l  7436  recexprlemss1u  7437  cauappcvgprlemdisj  7452  mulcmpblnr  7542  ltsrprg  7548  mulextsr1lem  7581  map2psrprg  7606  apreap  8342  mulext1  8367  mulext  8369  mulge0  8374  recexap  8407  lemul12b  8612  mulgt1  8614  lbreu  8696  nnrecgt0  8751  bndndx  8969  uzind  9155  fzind  9159  fnn0ind  9160  xlesubadd  9659  icoshft  9766  zltaddlt1le  9782  fzen  9816  elfz1b  9863  elfz0fzfz0  9896  elfzmlbp  9902  fzo1fzo0n0  9953  elfzo0z  9954  fzofzim  9958  elfzodifsumelfzo  9971  modqadd1  10127  modqmul1  10143  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  monoord  10242  seq3coll  10578  caucvgrelemcau  10745  caucvgre  10746  absext  10828  absle  10854  cau3lem  10879  icodiamlt  10945  climuni  11055  mulcn2  11074  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  dvds2lem  11494  dvdsabseq  11534  dfgcd2  11691  algcvga  11721  coprmgcdb  11758  coprmdvds2  11763  isprm3  11788  prmdvdsfz  11808  coprm  11811  rpexp12i  11822  sqrt2irr  11829  dfphi2  11885  strsetsid  11981  cncnp  12388  cncnp2m  12389  cnptopresti  12396  lmtopcnp  12408  txcnp  12429  txlm  12437  cnmptcom  12456  bldisj  12559  blssps  12585  blss  12586  metcnp3  12669  rescncf  12726  dedekindeulemloc  12755  dedekindicclemloc  12764  sincosq1lem  12895  sinq12gt0  12900  bj-sbimedh  12967  decidin  12993  bj-nnelirr  13140