ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syld Structured version   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  576  pm5.21ndd  620  mtord  696  pm5.11dc  814  anordc  862  hbimd  1462  alrimdd  1497  dral1  1615  sbiedh  1667  ax10oe  1675  sbequi  1717  sbcomxyyz  1843  mo2icl  2714  trel3  3853  poss  4026  sess2  4060  funun  4887  ssimaex  5177  f1imass  5356  isores3  5398  isoselem  5402  f1dmex  5685  f1o2ndf1  5791  smoel  5856  tfrlem9  5876  nntri1  6013  nnaordex  6036  ertr  6057  swoord2  6072  addnidpig  6320  ordpipqqs  6358  enq0tr  6416  prloc  6473  addnqprl  6512  addnqpru  6513  mulnqprl  6547  mulnqpru  6548  recexprlemss1l  6605  recexprlemss1u  6606  mulcmpblnr  6629  ltsrprg  6635  mulextsr1lem  6666  apreap  7331  mulext1  7356  mulext  7358  mulge0  7363  recexap  7376  lemul12b  7568  mulgt1  7570  nnrecgt0  7692  bndndx  7916  uzind  8085  fzind  8089  fnn0ind  8090  icoshft  8588  fzen  8637  elfz1b  8682  elfz0fzfz0  8713  elfzmlbmOLD  8719  elfzmlbp  8720  fzo1fzo0n0  8769  elfzo0z  8770  fzofzim  8774  elfzodifsumelfzo  8787  frecuzrdgfn  8839  iseqfveq2  8865  bj-sbimedh  9180  bj-nnelirr  9341
  Copyright terms: Public domain W3C validator