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  3852  poss  4025  sess2  4059  funun  4885  ssimaex  5175  f1imass  5354  isores3  5396  isoselem  5400  f1dmex  5682  f1o2ndf1  5788  smoel  5853  tfrlem9  5873  nntri1  6006  nnaordex  6029  ertr  6050  swoord2  6065  addnidpig  6313  ordpipqqs  6351  enq0tr  6409  prloc  6466  addnqprl  6505  addnqpru  6506  mulnqprl  6539  mulnqpru  6540  recexprlemss1l  6597  recexprlemss1u  6598  mulcmpblnr  6621  ltsrprg  6627  mulextsr1lem  6658  apreap  7323  mulext1  7348  mulext  7350  mulge0  7355  recexap  7368  lemul12b  7559  mulgt1  7561  nnrecgt0  7683  bndndx  7906  uzind  8074  fzind  8078  fnn0ind  8079  icoshft  8576  fzen  8623  elfz1b  8668  elfz0fzfz0  8699  elfzmlbmOLD  8705  elfzmlbp  8706  fzo1fzo0n0  8755  elfzo0z  8756  fzofzim  8760  elfzodifsumelfzo  8773  bj-sbimedh  8845  bj-nnelirr  9006
  Copyright terms: Public domain W3C validator