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  149  sylbid  150  sylibrd  169  sylbird  170  syland  293  animpimp2impd  561  nsyld  653  pm5.21ndd  713  mtord  791  pm2.521gdc  876  pm5.11dc  917  anordc  965  hbimd  1622  alrimdd  1658  dral1  1778  sbiedh  1835  ax10oe  1845  sbequi  1887  sbcomxyyz  2025  mo2icl  2986  trel3  4200  exmidsssnc  4299  poss  4401  sess2  4441  abnexg  4549  funun  5378  ssimaex  5716  f1imass  5925  isores3  5966  isoselem  5971  f1dmex  6287  f1o2ndf1  6402  suppssrst  6439  suppssrgst  6440  smoel  6509  tfrlem9  6528  nntri1  6707  nnaordex  6739  ertr  6760  swoord2  6775  findcard2s  7122  pr2ne  7440  addnidpig  7599  ordpipqqs  7637  enq0tr  7697  prloc  7754  addnqprl  7792  addnqpru  7793  mulnqprl  7831  mulnqpru  7832  recexprlemss1l  7898  recexprlemss1u  7899  cauappcvgprlemdisj  7914  mulcmpblnr  8004  ltsrprg  8010  mulextsr1lem  8043  map2psrprg  8068  apreap  8809  mulext1  8834  mulext  8836  mulge0  8841  recexap  8875  lemul12b  9083  mulgt1  9085  lbreu  9167  nnrecgt0  9223  bndndx  9443  uzind  9635  fzind  9639  fnn0ind  9640  xlesubadd  10162  icoshft  10269  zltaddlt1le  10287  fzen  10323  elfz1b  10370  elfz0fzfz0  10406  elfzmlbp  10412  fzo1fzo0n0  10468  elfzo0z  10469  fzofzim  10473  elfzodifsumelfzo  10492  modqadd1  10669  modqmul1  10685  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  monoord  10793  seqf1oglem1  10827  seqf1oglem2  10828  seq3coll  11152  ccatalpha  11239  swrdsbslen  11296  swrdspsleq  11297  swrdswrdlem  11334  swrdswrd  11335  pfxccatin12lem2a  11357  pfxccatin12lem1  11358  pfxccatin12lem3  11362  swrdccat3blem  11369  reuccatpfxs1lem  11376  caucvgrelemcau  11603  caucvgre  11604  absext  11686  absle  11712  cau3lem  11737  icodiamlt  11803  climuni  11916  mulcn2  11935  cvgratnnlemnexp  12148  cvgratnnlemmn  12149  fprodssdc  12214  p1modz1  12418  dvdsmodexp  12419  dvds2lem  12427  dvdsabseq  12471  bitsinv1lem  12585  dfgcd2  12648  algcvga  12686  coprmgcdb  12723  coprmdvds2  12728  isprm3  12753  prmdvdsfz  12774  coprm  12779  rpexp12i  12790  sqrt2irr  12797  dfphi2  12855  odzdvds  12881  pclemub  12923  pcprendvds  12926  pcpremul  12929  pcqcl  12942  pcdvdsb  12956  pcprmpw2  12969  difsqpwdvds  12974  pcaddlem  12975  pcmptcl  12978  pcfac  12986  prmpwdvds  12991  strsetsid  13178  imasabl  13986  lmodfopnelem2  14404  rnglidlmcl  14559  znunit  14738  cncnp  15024  cncnp2m  15025  cnptopresti  15032  lmtopcnp  15044  txcnp  15065  txlm  15073  cnmptcom  15092  bldisj  15195  blssps  15221  blss  15222  metcnp3  15305  rescncf  15375  dedekindeulemloc  15413  dedekindicclemloc  15422  sincosq1lem  15619  sinq12gt0  15624  logbgcd1irr  15761  lgsdir  15837  gausslemma2dlem6  15869  gausslemma2d  15871  lgsquadlem2  15880  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgslem3d1  15902  2sqlem6  15922  usgruspgrben  16110  subupgr  16197  upgrwlkvtxedg  16288  uspgr2wlkeq  16289  clwwlkext2edg  16346  clwwlknonex2lem2  16362  eupth2lemsfi  16402  bj-sbimedh  16472  decidin  16498  bj-charfunbi  16510  bj-nnelirr  16652