Theorem syld 27

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

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 117  sylibd 202  sylbid 203  sylibrd 204  sylbird 205  syland 457  syldan 467  sylan9 468  ax10o 1135  dral1 1150  cbv1 1158  sbied 1191  sbequi 1223  hbsb4 1243  ax11indalem 1361  ax11inda2ALT 1362  ralcom2 1768  trel3 2678  ralxfrd 2887  wefrc 2933  ordelord 2960  oninton 3002  orduniorsuc 3077  limuni3 3113  tfindsg 3152  funun 3540  f1dmex 3695  ssimaex 3753  fvopab3ig 3763  isomin 3884  isofrlem 3886  tfrlem2 3897  tfrlem9 3904  abianfp 3947  oprabvalig 4009  oaordi 4164  odi 4194  omass 4195  oeordi 4198  oeordsuc 4205  ecopoprtrn 4295  f1domg 4377  pwuninelg 4467  onomeneq 4498  pssnn 4513  unblem3 4519  isfinite2 4523  unfi 4528  inf3lem3 4587  inf3lem5 4589  r1tr 4626  rankr1 4646  rankval3 4653  rankxpsuc 4687  zorn2lem2 4761  zorn2lem3 4762  imadomg 4778  carduni 4830  alephle 4856  cardaleph 4857  iscard3 4860  alephfp 4872  axacndlem4 4934  addnidpi 5000  ordpipq 5028  ltbtwnpq 5056  genpnnp 5080  addclprlem1 5090  addclprlem2 5091  mulclprlem 5093  distrlem1pr 5099  distrlem2pr 5100  distrlem4pr 5102  psslinpr 5107  ltaddpr2 5113  ltexprlem6 5119  ltexpri 5121  addcanpr 5124  suplem2pr 5134  ltsrpr 5158  mulgt0sr 5186  recexsr 5188  suppsrlem 5193  suprelem 5231  axrrecex 5256  letrt 5498  xrletrt 5537  recext 5657  lemul12ait 5798  lemul12itOLD 5799  mulgt1t 5801  ltdivmult 5819  ledivmult 5820  nnrecgt0t 5900  lbreu 5992  nnunb 6017  bndndx 6020  xrub 6027  supxrunb1 6036  lt0nnn0 6063  elnnz1 6102  zeot 6146  uzind 6153  uzwo5OLD 6159  uzwo3lem1 6164  uzwo3lem2 6165  zmax 6168  qbtwnre 6216  qsqueeze 6218  icoshft 6341  fsequb 6455  fsequb2 6456  seqzfveq 6486  expordit 6531  expnbndt 6585  seq1bnd 6847  seq1ublem 6848  cau3ir 6852  faclbnd4lem4 6888  facavgt 6892  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  fsumcom 6966  fsumrev 6967  fsummulc1 6971  fsumcmp 6978  fsumabs 6981  clm4le 7019  2climnn 7039  2climnn0 7040  climaddlem3 7052  climmullem8 7063  climsup 7091  climcau 7092  caucvglem2 7094  caucvglem4 7096  caucvglem6 7098  caucvg 7099  serzf0 7105  ser1f0 7106  ser1cmp2lem 7112  isummulc1 7147  infcvglem3 7158  cvgratlem4 7188  fsum0diag2 7194  fsum0diag4 7196  rescncf 7207  ivthlem7 7222  ivthlem9 7224  ivthlem7OLD 7231  znnenlemOLD 7444  znnen 7445  unbenlem 7447  infxpidmlem7 7501  infxpidmlem8 7502  infxpidmlem12 7506  clsval2 7627  cncnplem4 7716  opnin 7809  metcnp 7826  metcnss2 7838  lmnn 7873  iscau3 7876  lmuni 7886  lmsslem 7887  lmle 7895  metcnp4lem2 7903  iscms2lem4 7926  lmcau 7930  cmsss 7931  bcthlem2 7934  bcthlem16 7948  bcthlem17 7949  isgrp 7975  grplactf1o 8034  ubthlem5 8464  ubthlem6 8465  minveclem27 8502  sincosq1lem 8620  sinq12gt0t 8625  normgt0tOLD 8914  normgt0t 8915  hcau2 8976  occon2t 9077  occllem6 9094  projlem26 9127  projlem28 9129  shmods 9277  spansneleq 9409  spansneleqOLD 9410  h1datom 9421  pjjs 9562  hmopidmch 9990  pjnormss 10007  stadd 10083  stm1add3 10084  stadd3 10085  golem2 10109  cvnsymt 10127  dmdmdt 10137  mdslmd1lem1 10160  mdslmd1 10164  mdexch 10170  atcveq0 10183  superpos 10189  hatomistic 10197  atexcht 10216  atoml2 10218  atcvat2 10222  irredlem1 10225  atcvat3 10231  mdsymlem3 10240  mdsymlem5 10242  cdj3lem2b 10269  cdj3 10273  ghomf1olem 10301  homcard 10426  rdmob 10525  cmpmorp 10556  cmphmia 10570  cmphmib 10571  homgrf 10574  ismonc 10584  cmpmon 10585

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

Copyright terms: Public domain