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:  syldc  45  3syld  56  sylsyld  57  sylibd  147  sylbid  148  sylibrd  167  sylbird  168  syland  287  animpimp2impd  526  nsyld  612  pm5.21ndd  656  mtord  732  pm5.11dc  853  anordc  902  hbimd  1510  alrimdd  1545  dral1  1665  sbiedh  1717  ax10oe  1725  sbequi  1767  sbcomxyyz  1894  mo2icl  2792  trel3  3936  poss  4116  sess2  4156  funun  5044  ssimaex  5349  f1imass  5535  isores3  5576  isoselem  5581  f1dmex  5869  f1o2ndf1  5975  smoel  6047  tfrlem9  6066  nntri1  6239  nnaordex  6266  ertr  6287  swoord2  6302  findcard2s  6586  pr2ne  6799  addnidpig  6874  ordpipqqs  6912  enq0tr  6972  prloc  7029  addnqprl  7067  addnqpru  7068  mulnqprl  7106  mulnqpru  7107  recexprlemss1l  7173  recexprlemss1u  7174  cauappcvgprlemdisj  7189  mulcmpblnr  7266  ltsrprg  7272  mulextsr1lem  7304  apreap  8040  mulext1  8065  mulext  8067  mulge0  8072  recexap  8096  lemul12b  8294  mulgt1  8296  lbreu  8378  nnrecgt0  8431  bndndx  8642  uzind  8827  fzind  8831  fnn0ind  8832  icoshft  9376  zltaddlt1le  9392  fzen  9426  elfz1b  9471  elfz0fzfz0  9502  elfzmlbp  9508  fzo1fzo0n0  9559  elfzo0z  9560  fzofzim  9564  elfzodifsumelfzo  9577  modqadd1  9733  modqmul1  9749  frecuzrdgtcl  9784  frecuzrdgfunlem  9791  iseqfveq2  9855  iseqshft2  9863  monoord  9869  iseqsplit  9873  iseqid2  9906  iseqcoll  10212  caucvgrelemcau  10378  caucvgre  10379  absext  10461  absle  10487  cau3lem  10512  icodiamlt  10578  climuni  10645  mulcn2  10665  cvgratnnlemnexp  10879  cvgratnnlemmn  10880  dvds2lem  10901  dvdsabseq  10941  dfgcd2  11096  ialgcvga  11126  coprmgcdb  11163  coprmdvds2  11168  isprm3  11193  prmdvdsfz  11213  coprm  11216  rpexp12i  11227  sqrt2irr  11234  dfphi2  11289  bj-sbimedh  11329  decidin  11354  bj-nnelirr  11505
  Copyright terms: Public domain W3C validator