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  1595  alrimdd  1631  dral1  1752  sbiedh  1809  ax10oe  1819  sbequi  1861  sbcomxyyz  1999  mo2icl  2951  trel3  4149  exmidsssnc  4246  poss  4343  sess2  4383  abnexg  4491  funun  5312  ssimaex  5634  f1imass  5833  isores3  5874  isoselem  5879  f1dmex  6191  f1o2ndf1  6304  smoel  6376  tfrlem9  6395  nntri1  6572  nnaordex  6604  ertr  6625  swoord2  6640  findcard2s  6969  pr2ne  7282  addnidpig  7431  ordpipqqs  7469  enq0tr  7529  prloc  7586  addnqprl  7624  addnqpru  7625  mulnqprl  7663  mulnqpru  7664  recexprlemss1l  7730  recexprlemss1u  7731  cauappcvgprlemdisj  7746  mulcmpblnr  7836  ltsrprg  7842  mulextsr1lem  7875  map2psrprg  7900  apreap  8642  mulext1  8667  mulext  8669  mulge0  8674  recexap  8708  lemul12b  8916  mulgt1  8918  lbreu  9000  nnrecgt0  9056  bndndx  9276  uzind  9466  fzind  9470  fnn0ind  9471  xlesubadd  9987  icoshft  10094  zltaddlt1le  10111  fzen  10147  elfz1b  10194  elfz0fzfz0  10230  elfzmlbp  10236  fzo1fzo0n0  10288  elfzo0z  10289  fzofzim  10293  elfzodifsumelfzo  10311  modqadd1  10487  modqmul1  10503  frecuzrdgtcl  10538  frecuzrdgfunlem  10545  monoord  10611  seqf1oglem1  10645  seqf1oglem2  10646  seq3coll  10968  caucvgrelemcau  11210  caucvgre  11211  absext  11293  absle  11319  cau3lem  11344  icodiamlt  11410  climuni  11523  mulcn2  11542  cvgratnnlemnexp  11754  cvgratnnlemmn  11755  fprodssdc  11820  p1modz1  12024  dvdsmodexp  12025  dvds2lem  12033  dvdsabseq  12077  bitsinv1lem  12191  dfgcd2  12254  algcvga  12292  coprmgcdb  12329  coprmdvds2  12334  isprm3  12359  prmdvdsfz  12380  coprm  12385  rpexp12i  12396  sqrt2irr  12403  dfphi2  12461  odzdvds  12487  pclemub  12529  pcprendvds  12532  pcpremul  12535  pcqcl  12548  pcdvdsb  12562  pcprmpw2  12575  difsqpwdvds  12580  pcaddlem  12581  pcmptcl  12584  pcfac  12592  prmpwdvds  12597  strsetsid  12784  imasabl  13590  lmodfopnelem2  14005  rnglidlmcl  14160  znunit  14339  cncnp  14620  cncnp2m  14621  cnptopresti  14628  lmtopcnp  14640  txcnp  14661  txlm  14669  cnmptcom  14688  bldisj  14791  blssps  14817  blss  14818  metcnp3  14901  rescncf  14971  dedekindeulemloc  15009  dedekindicclemloc  15018  sincosq1lem  15215  sinq12gt0  15220  logbgcd1irr  15357  lgsdir  15430  gausslemma2dlem6  15462  gausslemma2d  15464  lgsquadlem2  15473  2lgslem3a1  15492  2lgslem3b1  15493  2lgslem3c1  15494  2lgslem3d1  15495  2sqlem6  15515  bj-sbimedh  15571  decidin  15597  bj-charfunbi  15611  bj-nnelirr  15753