Theorem syld 30

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

Notice that syld 30 can be obtained from syl 12 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 28	. 2 |- (ph -> ((ps -> ch) -> (ps -> th)))
4	1, 3	mpd 29	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3

This theorem is referenced by:  3syld 31  sylsyld 32  imim12dOLD 70  nsyld 132  sylibd 219  sylbid 220  sylibrd 221  sylbird 222  syland 506  syldan 516  sylan9OLD 518  dral1 1515  cbv1 1523  sbied 1563  sbiedOLD 1564  sbequi 1598  hbsb4 1620  ax11indalem 1759  ax11inda2ALT 1760  ralcom2OLD 2245  trel3 3420  wefrc 3652  ordelord 3680  ralxfrd 3837  oninton 3881  orduniorsuc 3909  limuni3 3936  tfindsg 3944  funun 4462  f1dmex 4664  ssimaex 4729  fvopab3ig 4741  isomin 4876  isofrlem 4878  oprabvalig 4953  tfrlem9 5127  abianfp 5171  odi 5258  omass 5259  oeordi 5262  oeordsuc 5269  ecopoprtrn 5370  f1domg 5455  ac6sfilem3 5508  domtriord 5546  pwuninel 5550  2pwuninel 5551  onomeneq 5612  pssnn 5628  unblem3 5635  isfinite2 5639  ordiso 5683  ordtypelem2 5685  ordtypelem3 5686  ordtypelem5 5688  ordtypelem6 5689  inf3lem3 5721  inf3lem5 5723  r1tr 5765  rankr1 5785  rankval3 5792  rankxpsuc 5826  omsubsdomlem2 5880  omsubdom 5882  omsubindss 5888  zorn2lem2 5951  zorn2lem3 5952  imadomg 5968  carduni 6010  alephle 6032  iscard3 6036  alephfp 6048  axacndlem4 6114  addnidpi 6180  ltbtwnpq 6236  genpnnp 6260  addclprlem1 6270  addclprlem2 6271  mulclprlem 6273  distrlem1pr 6279  distrlem2pr 6280  psslinpr 6287  ltaddpr2 6293  ltexprlem6 6299  ltexpri 6301  addcanpr 6304  suplem2pr 6314  mulgt0sr 6366  recexsr 6368  suppsrlem 6373  suprelem 6411  axrrecex 6437  letr 6695  xrletr 6739  recex 6876  lemul12b 7024  lemul12aOLD 7025  mulgt1 7027  ltdivmulOLD 7050  ledivmulOLD 7052  nnrecgt0 7137  lbreu 7254  nnunb 7279  bndndx 7282  supxrunb1 7298  lt0nnn0 7325  elnnz1 7364  zeo 7411  uzind 7417  uzwo5OLD 7423  uzwo3lem1 7429  uzwo3lem2 7430  zmax 7433  qbtwnre 7459  qsqueeze 7461  modadd1 7518  modmul1 7519  icoshft 7577  fzen 7664  fsequb 7702  fsequb2 7703  seqzfveq 7797  expordi 7845  expnbnd 7901  seq1bndi 8162  seq1ublem 8163  cau3iri 8167  faclbnd4lem4 8203  fsum1ps 8278  fsumsplit 8280  fsumadd 8282  fsumcom 8288  fsumrev 8289  fsummulc1 8293  fsumcmp 8300  fsumabs 8303  clm4lei 8341  2climnn 8362  2climnn0 8363  climaddlem3 8376  climmullem8 8387  climsupi 8415  climcaui 8416  caucvglem2 8418  caucvglem4 8420  caucvglem6 8422  caucvgi 8423  serzf0i 8429  ser1cmp2lem 8436  isummulc1 8473  infcvglem3 8484  fsum0diag2 8521  fsum0diag4 8523  rescncf 8534  ivthlem7 8549  ivthlem9 8551  znnen 8771  unbenlem 8773  infxpidmlem7 8827  infxpidmlem8 8828  infxpidmlem12 8832  clsval2 8961  cncnplem4 9054  opnin 9146  metequiv 9158  metcnp 9165  metcnss2 9177  lmnn 9213  iscau3 9216  iscau4 9218  lmuni 9229  lmsslem 9230  lmle 9238  metcnp4lem2 9247  iscms2lem4 9270  lmcau 9274  cmsss 9275  bcthlem16 9292  bcthlem17 9293  isgrp 9321  grplactf1o 9406  gapm 9462  vacnlem3 9669  ubthlem5 9876  ubthlem6 9877  minveclem27 9916  sincosq1lem 10052  sinq12gt0t 10057  dif1en 10172  indexfi 10174  ficard 10176  dif1card 10177  txcn 10227  fbfgss 10288  filrn 10293  hausfillim 10303  flimopn 10321  fbaslim 10322  cncomp 10331  opidon 10369  rngmgmbs4 10401  normgt0OLD 10626  normgt0 10627  hcau2 10688  occllem6 10811  projlem26 10844  projlem28 10846  shmodsi 10995  spansneleq 11126  h1datomi 11137  pjjsi 11280  hmopidmchi 11723  pjnormssi 11740  stm1add3i 11819  golem2 11844  cvnsym 11862  dmdmd 11872  mdslmd1lem1 11897  mdslmd1i 11901  mdexchi 11907  atcveq0 11920  superpos 11926  hatomistici 11934  atoml2i 11955  atcvat2i 11959  irredlem1 11962  atcvat3i 11968  mdsymlem3 11977  mdsymlem5 11979  cdj3lem2b 12009  cdj3i 12013  bnj72 13208  fzind 13610  fnn0ind 13611  ghomf1olem 13637  ublbneg 13653  lbzbi 13657  dvds1lem 13666  dvds2lem 13667  dvdslelem 13692  divalglem8 13703  algcvga 13747  isprm3 13776  coprm 13782  fundmpss 13836  dfon2lem3 13851  dfon2lem6 13854  axext4dist 13867  setlikess 13906  tz6.26 13913  frmin 13938  soxp 13950  soseq 13955  wfrlem12 13968  sltval2 13997  axdenselem4 14022  axdenselem8 14026  axfelem5 14035  axfelem12 14042  axfelem17 14047  ubpar 14603  latdir 14643  fprod1ib 14686  homcard 14893  homindlem3 14900  bwt2 14960  cntrsetlem 14999  rdmob 15095  cmpmorp 15126  cmphmia 15147  cmphmib 15148  homgrf 15151  ismonc 15163  cmpmon 15164  iepiclem 15172  isepic 15173  idfisf 15189  elincin 15220  carinttar 15279  dmsdtriordOLD 15360  finminlem 15367  inficlALT 15372  finsschain 15373  ordisoOLD 15374  ordtypelem2OLD 15376  ordtypelem3OLD 15377  ordtypelem5OLD 15379  ordtypelem6OLD 15380  omsubsdomlem2OLD 15389  omsubdomOLD 15391  omsubindssOLD 15397  opncldf1 15402  cldbnd 15410  clsint2 15414  compsublem 15430  compsub 15431  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  alexsub 15441  dfcon2 15442  connsub 15443  cnconn 15444  reconnlem4 15449  reconnlem5 15450  reconn 15451  2ndcctbss 15478  reftr 15497  topfneec2 15502  fnessref 15503  locfincomp 15514  locfincf 15516  comppfsc 15517  neibastop1 15518  neibastop2lem3 15521  neibastop3 15524  topmtcl 15525  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  ist1-2 15542  ist1-3 15543  fgmin 15558  isufil2 15565  ufprim 15569  filssufillem 15570  fixufil 15576  filcon 15580  limfilcf 15587  cnpfillim 15589  fmfnfmlem2 15595  fmfnfmlem4 15597  fmfnfm 15598  fclusnei 15607  fcluscf 15612  flimfcls 15613  flimfnfcls 15615  fcluscnplem 15617  fcluscnp 15618  fcluscomplem 15620  fcluscomp 15621  isfclusf 15625  fclusfnei 15626  enf1f1o 15720  fimax 15746  indexfiOLD 15755  inficl 15757  frfi 15771  filbcmb 15776  seq1eq2 15817  nninfnub 15819  fsum00 15820  fsumlt 15821  blhalf 15846  mettrifi 15847  mettrifi2 15848  geomcau 15849  icoopnst 15876  iocopnst 15877  paste 15893  lmtlm 15908  sstotbnd 15936  totbndss 15937  totbndbnd 15944  ismtyhmeolem 15950  ismtybnd 15953  heiborlem1 15955  heiborlem13 15967  heiborlem16 15970  heiborlem23 15977  heiborlem32 15986  heiborlem35 15989  heiborlem36 15990  bfplem6 16003  rrnmet 16016  rrncms 16019  pcohtpy 16083  pcopt 16084  riscer 16142  crnghomfo 16154  keridl 16180  ispridl2 16186  ispridlc 16218  prtlem10 16265  ordpss 16428  smoel 16451  pwtr 16647  hlatmstc 17047  hlrelat1 17049  hlrelat2 17052  cvrexchlem 17059  cvratlem 17061  cvrat2 17066  atltcvr 17072  cvrat3 17075  cvrat4 17076  ps-1 17078  ps2 17079  pmapjoin 17313

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

Copyright terms: Public domain