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

Theorem syld 44
Description: Syllogism deduction.

Notice that syld 44 has the same form as syl 14 with  ph added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace  ph 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  |-  ( ph  ->  ( ps  ->  ch ) )
syld.2  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
syld  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syld
StepHypRef Expression
1 syld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syld.2 . . 3  |-  ( ph  ->  ( ch  ->  th )
)
32a1d 22 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
41, 3mpdd 40 1  |-  ( ph  ->  ( ps  ->  th )
)
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  2743  trel3  3890  poss  4063  sess2  4103  funun  4972  ssimaex  5262  f1imass  5441  isores3  5483  isoselem  5487  f1dmex  5771  f1o2ndf1  5877  smoel  5946  tfrlem9  5966  nntri1  6105  nnaordex  6131  ertr  6152  swoord2  6167  findcard2s  6378  addnidpig  6492  ordpipqqs  6530  enq0tr  6590  prloc  6647  addnqprl  6685  addnqpru  6686  mulnqprl  6724  mulnqpru  6725  recexprlemss1l  6791  recexprlemss1u  6792  cauappcvgprlemdisj  6807  mulcmpblnr  6884  ltsrprg  6890  mulextsr1lem  6922  apreap  7652  mulext1  7677  mulext  7679  mulge0  7684  recexap  7708  lemul12b  7902  mulgt1  7904  nnrecgt0  8027  bndndx  8238  uzind  8408  fzind  8412  fnn0ind  8413  icoshft  8959  zltaddlt1le  8975  fzen  9009  elfz1b  9054  elfz0fzfz0  9085  elfzmlbmOLD  9091  elfzmlbp  9092  fzo1fzo0n0  9141  elfzo0z  9142  fzofzim  9146  elfzodifsumelfzo  9159  modqadd1  9311  modqmul1  9327  frecuzrdgfn  9362  iseqfveq2  9392  iseqshft2  9396  monoord  9399  iseqsplit  9402  caucvgrelemcau  9807  caucvgre  9808  absext  9890  absle  9916  cau3lem  9941  icodiamlt  10007  climuni  10045  mulcn2  10064  dvds2lem  10120  dvdsabseq  10159  sqrt2irr  10251  ialgcvga  10273  bj-sbimedh  10298  bj-nnelirr  10465
  Copyright terms: Public domain W3C validator