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:  3syld  55  sylsyld  56  sylibd  142  sylbid  143  sylibrd  162  sylbird  163  syland  281  nsyld  587  pm5.21ndd  631  mtord  707  pm5.11dc  826  anordc  874  hbimd  1481  alrimdd  1516  dral1  1634  sbiedh  1686  ax10oe  1694  sbequi  1736  sbcomxyyz  1862  mo2icl  2742  trel3  3889  poss  4062  sess2  4102  funun  4971  ssimaex  5261  f1imass  5440  isores3  5482  isoselem  5486  f1dmex  5770  f1o2ndf1  5876  smoel  5945  tfrlem9  5965  nntri1  6104  nnaordex  6130  ertr  6151  swoord2  6166  findcard2s  6377  addnidpig  6491  ordpipqqs  6529  enq0tr  6589  prloc  6646  addnqprl  6684  addnqpru  6685  mulnqprl  6723  mulnqpru  6724  recexprlemss1l  6790  recexprlemss1u  6791  cauappcvgprlemdisj  6806  mulcmpblnr  6883  ltsrprg  6889  mulextsr1lem  6921  apreap  7651  mulext1  7676  mulext  7678  mulge0  7683  recexap  7707  lemul12b  7901  mulgt1  7903  nnrecgt0  8026  bndndx  8237  uzind  8407  fzind  8411  fnn0ind  8412  icoshft  8958  zltaddlt1le  8974  fzen  9008  elfz1b  9053  elfz0fzfz0  9084  elfzmlbmOLD  9090  elfzmlbp  9091  fzo1fzo0n0  9140  elfzo0z  9141  fzofzim  9145  elfzodifsumelfzo  9158  modqadd1  9310  modqmul1  9326  frecuzrdgfn  9361  iseqfveq2  9391  iseqshft2  9395  monoord  9398  iseqsplit  9401  caucvgrelemcau  9806  caucvgre  9807  absext  9889  absle  9915  cau3lem  9940  icodiamlt  10006  climuni  10044  mulcn2  10063  dvds2lem  10119  dvdsabseq  10158  sqrt2irr  10230  ialgcvga  10252  bj-sbimedh  10277  bj-nnelirr  10444
  Copyright terms: Public domain W3C validator