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  1777  sbiedh  1834  ax10oe  1844  sbequi  1886  sbcomxyyz  2024  mo2icl  2984  trel3  4196  exmidsssnc  4295  poss  4397  sess2  4437  abnexg  4545  funun  5373  ssimaex  5710  f1imass  5920  isores3  5961  isoselem  5966  f1dmex  6283  f1o2ndf1  6398  smoel  6471  tfrlem9  6490  nntri1  6669  nnaordex  6701  ertr  6722  swoord2  6737  findcard2s  7084  pr2ne  7402  addnidpig  7561  ordpipqqs  7599  enq0tr  7659  prloc  7716  addnqprl  7754  addnqpru  7755  mulnqprl  7793  mulnqpru  7794  recexprlemss1l  7860  recexprlemss1u  7861  cauappcvgprlemdisj  7876  mulcmpblnr  7966  ltsrprg  7972  mulextsr1lem  8005  map2psrprg  8030  apreap  8772  mulext1  8797  mulext  8799  mulge0  8804  recexap  8838  lemul12b  9046  mulgt1  9048  lbreu  9130  nnrecgt0  9186  bndndx  9406  uzind  9596  fzind  9600  fnn0ind  9601  xlesubadd  10123  icoshft  10230  zltaddlt1le  10247  fzen  10283  elfz1b  10330  elfz0fzfz0  10366  elfzmlbp  10372  fzo1fzo0n0  10428  elfzo0z  10429  fzofzim  10433  elfzodifsumelfzo  10452  modqadd1  10629  modqmul1  10645  frecuzrdgtcl  10680  frecuzrdgfunlem  10687  monoord  10753  seqf1oglem1  10787  seqf1oglem2  10788  seq3coll  11112  ccatalpha  11199  swrdsbslen  11256  swrdspsleq  11257  swrdswrdlem  11294  swrdswrd  11295  pfxccatin12lem2a  11317  pfxccatin12lem1  11318  pfxccatin12lem3  11322  swrdccat3blem  11329  reuccatpfxs1lem  11336  caucvgrelemcau  11563  caucvgre  11564  absext  11646  absle  11672  cau3lem  11697  icodiamlt  11763  climuni  11876  mulcn2  11895  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  fprodssdc  12174  p1modz1  12378  dvdsmodexp  12379  dvds2lem  12387  dvdsabseq  12431  bitsinv1lem  12545  dfgcd2  12608  algcvga  12646  coprmgcdb  12683  coprmdvds2  12688  isprm3  12713  prmdvdsfz  12734  coprm  12739  rpexp12i  12750  sqrt2irr  12757  dfphi2  12815  odzdvds  12841  pclemub  12883  pcprendvds  12886  pcpremul  12889  pcqcl  12902  pcdvdsb  12916  pcprmpw2  12929  difsqpwdvds  12934  pcaddlem  12935  pcmptcl  12938  pcfac  12946  prmpwdvds  12951  strsetsid  13138  imasabl  13946  lmodfopnelem2  14363  rnglidlmcl  14518  znunit  14697  cncnp  14983  cncnp2m  14984  cnptopresti  14991  lmtopcnp  15003  txcnp  15024  txlm  15032  cnmptcom  15051  bldisj  15154  blssps  15180  blss  15181  metcnp3  15264  rescncf  15334  dedekindeulemloc  15372  dedekindicclemloc  15381  sincosq1lem  15578  sinq12gt0  15583  logbgcd1irr  15720  lgsdir  15793  gausslemma2dlem6  15825  gausslemma2d  15827  lgsquadlem2  15836  2lgslem3a1  15855  2lgslem3b1  15856  2lgslem3c1  15857  2lgslem3d1  15858  2sqlem6  15878  usgruspgrben  16066  subupgr  16153  upgrwlkvtxedg  16244  uspgr2wlkeq  16245  clwwlkext2edg  16302  clwwlknonex2lem2  16318  eupth2lemsfi  16358  bj-sbimedh  16428  decidin  16454  bj-charfunbi  16466  bj-nnelirr  16608