ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syld GIF version

Theorem syld 40
Description: Syllogism deduction.

Notice that syld 40 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
StepHypRef Expression
1 syld.1 . 2 (𝜑 → (𝜓𝜒))
2 syld.2 . . 3 (𝜑 → (𝜒𝜃))
32a1d 22 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
41, 3mpdd 36 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  3syld  51  sylsyld  52  sylibd  138  sylbid  139  sylibrd  158  sylbird  159  syland  277  nsyld  577  pm5.21ndd  621  mtord  697  pm5.11dc  815  anordc  863  hbimd  1465  alrimdd  1500  dral1  1618  sbiedh  1670  ax10oe  1678  sbequi  1720  sbcomxyyz  1846  mo2icl  2720  trel3  3862  poss  4035  sess2  4075  funun  4944  ssimaex  5234  f1imass  5413  isores3  5455  isoselem  5459  f1dmex  5743  f1o2ndf1  5849  smoel  5915  tfrlem9  5935  nntri1  6074  nnaordex  6100  ertr  6121  swoord2  6136  findcard2s  6347  addnidpig  6432  ordpipqqs  6470  enq0tr  6530  prloc  6587  addnqprl  6625  addnqpru  6626  mulnqprl  6664  mulnqpru  6665  recexprlemss1l  6731  recexprlemss1u  6732  cauappcvgprlemdisj  6747  mulcmpblnr  6824  ltsrprg  6830  mulextsr1lem  6862  apreap  7576  mulext1  7601  mulext  7603  mulge0  7608  recexap  7632  lemul12b  7825  mulgt1  7827  nnrecgt0  7949  bndndx  8178  uzind  8347  fzind  8351  fnn0ind  8352  icoshft  8856  fzen  8905  elfz1b  8950  elfz0fzfz0  8981  elfzmlbmOLD  8987  elfzmlbp  8988  fzo1fzo0n0  9037  elfzo0z  9038  fzofzim  9042  elfzodifsumelfzo  9055  frecuzrdgfn  9172  iseqfveq2  9202  iseqshft2  9206  monoord  9209  iseqsplit  9212  caucvgrelemcau  9553  caucvgre  9554  absext  9635  absle  9659  cau3lem  9684  icodiamlt  9750  climuni  9788  mulcn2  9807  sqrt2irr  9852  ialgcvga  9864  bj-sbimedh  9885  bj-nnelirr  10052
  Copyright terms: Public domain W3C validator