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

Theorem syld 44
Description: Syllogism deduction.

Notice that syld 44 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 40 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:  syldc  45  3syld  56  sylsyld  57  sylibd  147  sylbid  148  sylibrd  167  sylbird  168  syland  287  nsyld  610  pm5.21ndd  654  mtord  730  pm5.11dc  849  anordc  898  hbimd  1506  alrimdd  1541  dral1  1660  sbiedh  1712  ax10oe  1720  sbequi  1762  sbcomxyyz  1889  mo2icl  2781  trel3  3904  poss  4082  sess2  4122  funun  4995  ssimaex  5288  f1imass  5467  isores3  5508  isoselem  5512  f1dmex  5796  f1o2ndf1  5902  smoel  5971  tfrlem9  5990  nntri1  6162  nnaordex  6189  ertr  6210  swoord2  6225  findcard2s  6448  pr2ne  6597  addnidpig  6665  ordpipqqs  6703  enq0tr  6763  prloc  6820  addnqprl  6858  addnqpru  6859  mulnqprl  6897  mulnqpru  6898  recexprlemss1l  6964  recexprlemss1u  6965  cauappcvgprlemdisj  6980  mulcmpblnr  7057  ltsrprg  7063  mulextsr1lem  7095  apreap  7831  mulext1  7856  mulext  7858  mulge0  7863  recexap  7887  lemul12b  8083  mulgt1  8085  lbreu  8167  nnrecgt0  8220  bndndx  8431  uzind  8616  fzind  8620  fnn0ind  8621  icoshft  9165  zltaddlt1le  9181  fzen  9215  elfz1b  9260  elfz0fzfz0  9291  elfzmlbp  9297  fzo1fzo0n0  9346  elfzo0z  9347  fzofzim  9351  elfzodifsumelfzo  9364  modqadd1  9520  modqmul1  9536  frecuzrdgtcl  9571  frecuzrdgfunlem  9578  iseqfveq2  9621  iseqshft2  9625  monoord  9628  iseqsplit  9631  iseqid2  9641  caucvgrelemcau  10092  caucvgre  10093  absext  10175  absle  10201  cau3lem  10226  icodiamlt  10292  climuni  10358  mulcn2  10377  dvds2lem  10440  dvdsabseq  10480  dfgcd2  10635  ialgcvga  10665  coprmgcdb  10702  coprmdvds2  10707  isprm3  10732  prmdvdsfz  10752  coprm  10755  rpexp12i  10766  sqrt2irr  10773  dfphi2  10828  bj-sbimedh  10867  decidin  10892  bj-nnelirr  11040
  Copyright terms: Public domain W3C validator