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  559  nsyld  649  pm5.21ndd  706  mtord  784  pm2.521gdc  869  pm5.11dc  910  anordc  958  hbimd  1587  alrimdd  1623  dral1  1744  sbiedh  1801  ax10oe  1811  sbequi  1853  sbcomxyyz  1991  mo2icl  2943  trel3  4140  exmidsssnc  4237  poss  4334  sess2  4374  abnexg  4482  funun  5303  ssimaex  5625  f1imass  5824  isores3  5865  isoselem  5870  f1dmex  6182  f1o2ndf1  6295  smoel  6367  tfrlem9  6386  nntri1  6563  nnaordex  6595  ertr  6616  swoord2  6631  findcard2s  6960  pr2ne  7271  addnidpig  7420  ordpipqqs  7458  enq0tr  7518  prloc  7575  addnqprl  7613  addnqpru  7614  mulnqprl  7652  mulnqpru  7653  recexprlemss1l  7719  recexprlemss1u  7720  cauappcvgprlemdisj  7735  mulcmpblnr  7825  ltsrprg  7831  mulextsr1lem  7864  map2psrprg  7889  apreap  8631  mulext1  8656  mulext  8658  mulge0  8663  recexap  8697  lemul12b  8905  mulgt1  8907  lbreu  8989  nnrecgt0  9045  bndndx  9265  uzind  9454  fzind  9458  fnn0ind  9459  xlesubadd  9975  icoshft  10082  zltaddlt1le  10099  fzen  10135  elfz1b  10182  elfz0fzfz0  10218  elfzmlbp  10224  fzo1fzo0n0  10276  elfzo0z  10277  fzofzim  10281  elfzodifsumelfzo  10294  modqadd1  10470  modqmul1  10486  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  monoord  10594  seqf1oglem1  10628  seqf1oglem2  10629  seq3coll  10951  caucvgrelemcau  11162  caucvgre  11163  absext  11245  absle  11271  cau3lem  11296  icodiamlt  11362  climuni  11475  mulcn2  11494  cvgratnnlemnexp  11706  cvgratnnlemmn  11707  fprodssdc  11772  p1modz1  11976  dvdsmodexp  11977  dvds2lem  11985  dvdsabseq  12029  bitsinv1lem  12143  dfgcd2  12206  algcvga  12244  coprmgcdb  12281  coprmdvds2  12286  isprm3  12311  prmdvdsfz  12332  coprm  12337  rpexp12i  12348  sqrt2irr  12355  dfphi2  12413  odzdvds  12439  pclemub  12481  pcprendvds  12484  pcpremul  12487  pcqcl  12500  pcdvdsb  12514  pcprmpw2  12527  difsqpwdvds  12532  pcaddlem  12533  pcmptcl  12536  pcfac  12544  prmpwdvds  12549  strsetsid  12736  imasabl  13542  lmodfopnelem2  13957  rnglidlmcl  14112  znunit  14291  cncnp  14550  cncnp2m  14551  cnptopresti  14558  lmtopcnp  14570  txcnp  14591  txlm  14599  cnmptcom  14618  bldisj  14721  blssps  14747  blss  14748  metcnp3  14831  rescncf  14901  dedekindeulemloc  14939  dedekindicclemloc  14948  sincosq1lem  15145  sinq12gt0  15150  logbgcd1irr  15287  lgsdir  15360  gausslemma2dlem6  15392  gausslemma2d  15394  lgsquadlem2  15403  2lgslem3a1  15422  2lgslem3b1  15423  2lgslem3c1  15424  2lgslem3d1  15425  2sqlem6  15445  bj-sbimedh  15501  decidin  15527  bj-charfunbi  15541  bj-nnelirr  15683