Theorem syld 27

Description: Syllogism deduction. (The proof was shortened by O'Cat, 19-Feb-2008.)

Notice that syld 27 can be obtained from syl 10 by replacing each hypothesis and conclusion ta by (ph -> ta). In general, this process will always yield a new propositional calculus theorem because of something called the Deduction Theorem for propositional calculus.

Hypotheses

Ref	Expression
syld.1	|- (ph -> (ps -> ch))
syld.2	|- (ph -> (ch -> th))

Assertion

Ref	Expression
syld	|- (ph -> (ps -> th))

Proof of Theorem syld

Step	Hyp	Ref	Expression
1		syld.1	. 2 |- (ph -> (ps -> ch))
2		syld.2	. . 3 |- (ph -> (ch -> th))
3	2	imim2d 25	. 2 |- (ph -> ((ps -> ch) -> (ps -> th)))
4	1, 3	mpd 26	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  imim12d 29  nsyld 116  sylibd 200  sylbid 201  sylibrd 202  sylbird 203  syland 459  syldan 469  sylan9 470  ax10o 1176  dral1 1191  cbv1 1199  sbied 1232  sbequi 1265  hbsb4 1286  ax11indalem 1407  ax11inda2ALT 1408  ralcom2 1822  trel3 2762  wefrc 2970  ordelord 2997  ralxfrd 3120  oninton 3157  orduniorsuc 3184  limuni3 3206  tfindsg 3213  funun 3659  f1dmex 3821  ssimaex 3879  fvopab3ig 3889  isomin 4013  isofrlem 4015  oprabvalig 4084  onfununi 4209  tfrlem2 4213  tfrlem9 4220  abianfp 4263  oaordi 4316  odi 4346  omass 4347  oeordi 4350  oeordsuc 4357  ecopoprtrn 4452  f1domg 4537  ac6sfilem3 4590  pwuninel 4631  2pwuninel 4632  onomeneq 4665  pssnn 4681  unblem3 4688  isfinite2 4692  unfi 4697  inf3lem3 4760  inf3lem5 4762  r1tr 4800  rankr1 4820  rankval3 4827  rankxpsuc 4861  zorn2lem2 4935  zorn2lem3 4936  imadomg 4952  carduni 5008  alephle 5034  cardaleph 5035  iscard3 5038  alephfp 5050  axacndlem4 5116  addnidpi 5182  ordpipq 5210  ltbtwnpq 5238  genpnnp 5262  addclprlem1 5272  addclprlem2 5273  mulclprlem 5275  distrlem1pr 5281  distrlem2pr 5282  distrlem4pr 5284  psslinpr 5289  ltaddpr2 5295  ltexprlem6 5301  ltexpri 5303  addcanpr 5306  suplem2pr 5316  ltsrpr 5340  mulgt0sr 5368  recexsr 5370  suppsrlem 5375  suprelem 5413  axrrecex 5438  letr 5679  xrletr 5718  recex 5840  lemul12b 5986  lemul12aOLD 5987  mulgt1 5989  ltdivmulOLD 6012  ledivmulOLD 6014  nnrecgt0 6099  lbreu 6213  nnunb 6238  bndndx 6241  xrub 6248  supxrunb1 6257  lt0nnn0 6284  elnnz1 6323  zeo 6370  uzind 6376  uzwo5OLD 6382  uzwo3lem1 6388  uzwo3lem2 6389  zmax 6392  qbtwnre 6418  qsqueeze 6420  modadd1 6477  modmul1 6478  icoshft 6535  fzen 6622  fsequb 6654  fsequb2 6655  seqzfveq 6749  expordi 6797  expnbnd 6852  seq1bndi 7113  seq1ublem 7114  cau3iri 7118  faclbnd4lem4 7154  facavg 7158  fsum1ps 7221  fsumsplit 7223  fsumadd 7225  fsumcom 7231  fsumrev 7232  fsummulc1 7236  fsumcmp 7243  fsumabs 7246  clm4lei 7284  2climnn 7305  2climnn0 7306  climaddlem3 7319  climmullem8 7330  climsupi 7358  climcaui 7359  caucvglem2 7361  caucvglem4 7363  caucvglem6 7365  caucvgi 7366  serzf0i 7372  ser1cmp2lem 7379  isummulc1 7416  infcvglem3 7427  cvgratlem4 7458  fsum0diag2 7464  fsum0diag4 7466  rescncf 7477  ivthlem7 7492  ivthlem9 7494  znnen 7714  unbenlem 7716  infxpidmlem7 7770  infxpidmlem8 7771  infxpidmlem12 7775  clsval2 7895  cncnplem4 7987  opnin 8079  metequiv 8091  metcnp 8098  metcnss2 8110  lmnn 8146  iscau3 8149  iscau4 8151  lmuni 8162  lmsslem 8163  lmle 8171  metcnp4lem2 8180  iscms2lem4 8203  lmcau 8207  cmsss 8208  bcthlem2 8211  bcthlem16 8225  bcthlem17 8226  isgrp 8254  grplactf1o 8339  vacnlem3 8584  ubthlem5 8791  ubthlem6 8792  minveclem27 8831  sincosq1lem 8970  sinq12gt0t 8975  normgt0OLD 9269  normgt0 9270  hcau2 9331  occon2 9437  occllem6 9454  projlem26 9487  projlem28 9489  shmodsi 9638  spansneleq 9769  h1datomi 9780  pjjsi 9923  hmopidmchi 10359  pjnormssi 10376  staddi 10454  stm1add3i 10455  stadd3i 10456  golem2 10480  cvnsym 10498  dmdmd 10508  mdslmd1lem1 10533  mdslmd1i 10537  mdexchi 10543  atcveq0 10556  superpos 10562  hatomistici 10570  atexch 10590  atoml2i 10592  atcvat2i 10596  irredlem1 10599  atcvat3i 10605  mdsymlem3 10614  mdsymlem5 10616  cdj3lem2b 10646  cdj3i 10650  ghomf1olem 10681  opidon 10898  rngmgmbs4 10945  homcard 11045  homindlem3 11053  bwt2 11123  rdmob 11202  cmpmorp 11233  cmphmia 11253  cmphmib 11254  homgrf 11257  ismonc 11269  cmpmon 11270  iepiclem 11278  isepic 11279  idfisf 11295  3syld 11324  dmsdtriord 11408  finminlem 11418  inficlALT 11424  finsschain 11425  ordiso 11426  ordtypelem2 11428  ordtypelem3 11429  ordtypelem5 11431  ordtypelem6 11432  omsubsdomlem2 11441  omsubdom 11443  omsubindss 11449  opncldf1 11454  cldbnd 11462  clsint2 11466  compsublem 11487  compsub 11488  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  dfcon2 11501  connsub 11502  cnconn 11503  reconnlem4 11510  reconnlem5 11511  reconn 11512  2ndcctbss 11539  reftr 11558  topfneec2 11563  fnessref 11564  locfincomp 11575  locfincf 11577  comppfsc 11578  neibastop1 11579  neibastop2lem3 11582  neibastop3 11585  topmtcl 11586  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  ist1-2 11603  ist1-3 11604  fbunfip 11631  fgmin 11639  fbfgss 11640  filrn 11643  isufil2 11650  ufprim 11654  filssufillem 11655  fixufil 11661  filcon 11665  flimopn 11679  fbaslim 11680  limfilcf 11683  hausfillim 11685  cnpfillim 11686  fmfnfmlem2 11701  fmfnfmlem4 11703  fmfnfm 11704  fclusnei 11719  fcluscf 11724  flimfcls 11725  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomplem 11732  fcluscomp 11733  ufcomp 11734  isfclusf 11737  fclusfnei 11738  gapm 11784  ficard 11834  dif1card 11835  fimax 11837  fixp 11840  indexf 11847  inficl 11849  filbcmb 11857  nninfnub 11882  fsum00 11883  fsumlt 11884  blhalf 11911  mettrifi 11912  mettrifi2 11913  geomcau 11914  icoopnst 11940  iocopnst 11941  paste 11954  lmtlm 11969  txcn 11979  sstotbnd 11992  totbndss 11993  totbndbnd 12000  ismtyhmeolem 12006  ismtybnd 12009  heiborlem1 12011  heiborlem13 12023  heiborlem16 12026  heiborlem23 12033  heiborlem32 12042  heiborlem35 12045  heiborlem36 12046  bfplem6 12059  rrnmet 12072  rrncms 12075  rrntotbnd 12078

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain