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  712  mtord  790  pm2.521gdc  875  pm5.11dc  916  anordc  964  hbimd  1621  alrimdd  1657  dral1  1778  sbiedh  1835  ax10oe  1845  sbequi  1887  sbcomxyyz  2025  mo2icl  2985  trel3  4195  exmidsssnc  4293  poss  4395  sess2  4435  abnexg  4543  funun  5371  ssimaex  5707  f1imass  5915  isores3  5956  isoselem  5961  f1dmex  6278  f1o2ndf1  6393  smoel  6466  tfrlem9  6485  nntri1  6664  nnaordex  6696  ertr  6717  swoord2  6732  findcard2s  7079  pr2ne  7397  addnidpig  7556  ordpipqqs  7594  enq0tr  7654  prloc  7711  addnqprl  7749  addnqpru  7750  mulnqprl  7788  mulnqpru  7789  recexprlemss1l  7855  recexprlemss1u  7856  cauappcvgprlemdisj  7871  mulcmpblnr  7961  ltsrprg  7967  mulextsr1lem  8000  map2psrprg  8025  apreap  8767  mulext1  8792  mulext  8794  mulge0  8799  recexap  8833  lemul12b  9041  mulgt1  9043  lbreu  9125  nnrecgt0  9181  bndndx  9401  uzind  9591  fzind  9595  fnn0ind  9596  xlesubadd  10118  icoshft  10225  zltaddlt1le  10242  fzen  10278  elfz1b  10325  elfz0fzfz0  10361  elfzmlbp  10367  fzo1fzo0n0  10423  elfzo0z  10424  fzofzim  10428  elfzodifsumelfzo  10447  modqadd1  10624  modqmul1  10640  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  monoord  10748  seqf1oglem1  10782  seqf1oglem2  10783  seq3coll  11107  ccatalpha  11194  swrdsbslen  11251  swrdspsleq  11252  swrdswrdlem  11289  swrdswrd  11290  pfxccatin12lem2a  11312  pfxccatin12lem1  11313  pfxccatin12lem3  11317  swrdccat3blem  11324  reuccatpfxs1lem  11331  caucvgrelemcau  11545  caucvgre  11546  absext  11628  absle  11654  cau3lem  11679  icodiamlt  11745  climuni  11858  mulcn2  11877  cvgratnnlemnexp  12090  cvgratnnlemmn  12091  fprodssdc  12156  p1modz1  12360  dvdsmodexp  12361  dvds2lem  12369  dvdsabseq  12413  bitsinv1lem  12527  dfgcd2  12590  algcvga  12628  coprmgcdb  12665  coprmdvds2  12670  isprm3  12695  prmdvdsfz  12716  coprm  12721  rpexp12i  12732  sqrt2irr  12739  dfphi2  12797  odzdvds  12823  pclemub  12865  pcprendvds  12868  pcpremul  12871  pcqcl  12884  pcdvdsb  12898  pcprmpw2  12911  difsqpwdvds  12916  pcaddlem  12917  pcmptcl  12920  pcfac  12928  prmpwdvds  12933  strsetsid  13120  imasabl  13928  lmodfopnelem2  14345  rnglidlmcl  14500  znunit  14679  cncnp  14960  cncnp2m  14961  cnptopresti  14968  lmtopcnp  14980  txcnp  15001  txlm  15009  cnmptcom  15028  bldisj  15131  blssps  15157  blss  15158  metcnp3  15241  rescncf  15311  dedekindeulemloc  15349  dedekindicclemloc  15358  sincosq1lem  15555  sinq12gt0  15560  logbgcd1irr  15697  lgsdir  15770  gausslemma2dlem6  15802  gausslemma2d  15804  lgsquadlem2  15813  2lgslem3a1  15832  2lgslem3b1  15833  2lgslem3c1  15834  2lgslem3d1  15835  2sqlem6  15855  usgruspgrben  16043  subupgr  16130  upgrwlkvtxedg  16221  uspgr2wlkeq  16222  clwwlkext2edg  16279  clwwlknonex2lem2  16295  eupth2lemsfi  16335  bj-sbimedh  16393  decidin  16419  bj-charfunbi  16432  bj-nnelirr  16574