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

Theorem syld 45
Description: Syllogism deduction.

Notice that syld 45 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 41 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syldc  46  3syld  57  sylsyld  58  sylibd  148  sylbid  149  sylibrd  168  sylbird  169  syland  289  animpimp2impd  531  nsyld  620  pm5.21ndd  677  mtord  755  pm2.521gdc  836  pm5.11dc  877  anordc  923  hbimd  1535  alrimdd  1571  dral1  1691  sbiedh  1743  ax10oe  1751  sbequi  1793  sbcomxyyz  1921  mo2icl  2834  trel3  4002  exmidsssnc  4094  poss  4188  sess2  4228  abnexg  4335  funun  5135  ssimaex  5448  f1imass  5641  isores3  5682  isoselem  5687  f1dmex  5980  f1o2ndf1  6091  smoel  6163  tfrlem9  6182  nntri1  6358  nnaordex  6389  ertr  6410  swoord2  6425  findcard2s  6750  pr2ne  7014  addnidpig  7108  ordpipqqs  7146  enq0tr  7206  prloc  7263  addnqprl  7301  addnqpru  7302  mulnqprl  7340  mulnqpru  7341  recexprlemss1l  7407  recexprlemss1u  7408  cauappcvgprlemdisj  7423  mulcmpblnr  7513  ltsrprg  7519  mulextsr1lem  7552  map2psrprg  7577  apreap  8312  mulext1  8337  mulext  8339  mulge0  8344  recexap  8377  lemul12b  8579  mulgt1  8581  lbreu  8663  nnrecgt0  8718  bndndx  8930  uzind  9116  fzind  9120  fnn0ind  9121  xlesubadd  9617  icoshft  9724  zltaddlt1le  9740  fzen  9774  elfz1b  9821  elfz0fzfz0  9854  elfzmlbp  9860  fzo1fzo0n0  9911  elfzo0z  9912  fzofzim  9916  elfzodifsumelfzo  9929  modqadd1  10085  modqmul1  10101  frecuzrdgtcl  10136  frecuzrdgfunlem  10143  monoord  10200  seq3coll  10536  caucvgrelemcau  10703  caucvgre  10704  absext  10786  absle  10812  cau3lem  10837  icodiamlt  10903  climuni  11013  mulcn2  11032  cvgratnnlemnexp  11244  cvgratnnlemmn  11245  dvds2lem  11412  dvdsabseq  11452  dfgcd2  11609  algcvga  11639  coprmgcdb  11676  coprmdvds2  11681  isprm3  11706  prmdvdsfz  11726  coprm  11729  rpexp12i  11740  sqrt2irr  11747  dfphi2  11802  strsetsid  11898  cncnp  12305  cncnp2m  12306  cnptopresti  12313  lmtopcnp  12325  txcnp  12346  txlm  12354  cnmptcom  12373  bldisj  12476  blssps  12502  blss  12503  metcnp3  12586  rescncf  12643  dedekindeulemloc  12672  dedekindicclemloc  12681  bj-sbimedh  12812  decidin  12838  bj-nnelirr  12985
  Copyright terms: Public domain W3C validator