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  1584  alrimdd  1620  dral1  1741  sbiedh  1798  ax10oe  1808  sbequi  1850  sbcomxyyz  1984  mo2icl  2931  trel3  4124  exmidsssnc  4221  poss  4316  sess2  4356  abnexg  4464  funun  5279  ssimaex  5598  f1imass  5796  isores3  5837  isoselem  5842  f1dmex  6142  f1o2ndf1  6254  smoel  6326  tfrlem9  6345  nntri1  6522  nnaordex  6554  ertr  6575  swoord2  6590  findcard2s  6919  pr2ne  7222  addnidpig  7366  ordpipqqs  7404  enq0tr  7464  prloc  7521  addnqprl  7559  addnqpru  7560  mulnqprl  7598  mulnqpru  7599  recexprlemss1l  7665  recexprlemss1u  7666  cauappcvgprlemdisj  7681  mulcmpblnr  7771  ltsrprg  7777  mulextsr1lem  7810  map2psrprg  7835  apreap  8575  mulext1  8600  mulext  8602  mulge0  8607  recexap  8641  lemul12b  8849  mulgt1  8851  lbreu  8933  nnrecgt0  8988  bndndx  9206  uzind  9395  fzind  9399  fnn0ind  9400  xlesubadd  9915  icoshft  10022  zltaddlt1le  10039  fzen  10075  elfz1b  10122  elfz0fzfz0  10158  elfzmlbp  10164  fzo1fzo0n0  10215  elfzo0z  10216  fzofzim  10220  elfzodifsumelfzo  10233  modqadd1  10394  modqmul1  10410  frecuzrdgtcl  10445  frecuzrdgfunlem  10452  monoord  10509  seq3coll  10857  caucvgrelemcau  11024  caucvgre  11025  absext  11107  absle  11133  cau3lem  11158  icodiamlt  11224  climuni  11336  mulcn2  11355  cvgratnnlemnexp  11567  cvgratnnlemmn  11568  fprodssdc  11633  p1modz1  11836  dvdsmodexp  11837  dvds2lem  11845  dvdsabseq  11888  dfgcd2  12050  algcvga  12086  coprmgcdb  12123  coprmdvds2  12128  isprm3  12153  prmdvdsfz  12174  coprm  12179  rpexp12i  12190  sqrt2irr  12197  dfphi2  12255  odzdvds  12280  pclemub  12322  pcprendvds  12325  pcpremul  12328  pcqcl  12341  pcdvdsb  12355  pcprmpw2  12368  difsqpwdvds  12373  pcaddlem  12374  pcmptcl  12377  pcfac  12385  prmpwdvds  12390  strsetsid  12548  imasabl  13290  lmodfopnelem2  13658  rnglidlmcl  13813  cncnp  14207  cncnp2m  14208  cnptopresti  14215  lmtopcnp  14227  txcnp  14248  txlm  14256  cnmptcom  14275  bldisj  14378  blssps  14404  blss  14405  metcnp3  14488  rescncf  14545  dedekindeulemloc  14574  dedekindicclemloc  14583  sincosq1lem  14723  sinq12gt0  14728  logbgcd1irr  14862  lgsdir  14914  2sqlem6  14945  bj-sbimedh  15001  decidin  15027  bj-charfunbi  15041  bj-nnelirr  15183