ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syld Structured version   Unicode 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  6417  prloc  6474  addnqprl  6512  addnqpru  6513  mulnqprl  6549  mulnqpru  6550  recexprlemss1l  6607  recexprlemss1u  6608  cauappcvgprlemdisj  6623  mulcmpblnr  6669  ltsrprg  6675  mulextsr1lem  6706  apreap  7371  mulext1  7396  mulext  7398  mulge0  7403  recexap  7416  lemul12b  7608  mulgt1  7610  nnrecgt0  7732  bndndx  7956  uzind  8125  fzind  8129  fnn0ind  8130  icoshft  8628  fzen  8677  elfz1b  8722  elfz0fzfz0  8753  elfzmlbmOLD  8759  elfzmlbp  8760  fzo1fzo0n0  8809  elfzo0z  8810  fzofzim  8814  elfzodifsumelfzo  8827  frecuzrdgfn  8879  iseqfveq2  8905  bj-sbimedh  9246  bj-nnelirr  9413
  Copyright terms: Public domain W3C validator