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 1137  dral1 1152  cbv1 1160  sbied 1193  sbequi 1226  hbsb4 1246  ax11indalem 1366  ax11inda2ALT 1367  ralcom2 1773  trel3 2683  ralxfrd 2892  wefrc 2938  ordelord 2965  oninton 3007  orduniorsuc 3082  limuni3 3118  tfindsg 3157  funun 3546  f1dmex 3701  ssimaex 3759  fvopab3ig 3769  isomin 3890  isofrlem 3892  tfrlem2 3903  tfrlem9 3910  abianfp 3953  oprabvalig 4015  oaordi 4170  odi 4200  omass 4201  oeordi 4204  oeordsuc 4211  ecopoprtrn 4301  f1domg 4383  pwuninel 4472  2pwuninel 4473  onomeneq 4504  pssnn 4519  unblem3 4525  isfinite2 4529  unfi 4534  inf3lem3 4595  inf3lem5 4597  r1tr 4634  rankr1 4654  rankval3 4661  rankxpsuc 4695  zorn2lem2 4769  zorn2lem3 4770  imadomg 4786  carduni 4838  alephle 4864  cardaleph 4865  iscard3 4868  alephfp 4880  axacndlem4 4942  addnidpi 5008  ordpipq 5036  ltbtwnpq 5064  genpnnp 5088  addclprlem1 5098  addclprlem2 5099  mulclprlem 5101  distrlem1pr 5107  distrlem2pr 5108  distrlem4pr 5110  psslinpr 5115  ltaddpr2 5121  ltexprlem6 5127  ltexpri 5129  addcanpr 5132  suplem2pr 5142  ltsrpr 5166  mulgt0sr 5194  recexsr 5196  suppsrlem 5201  suprelem 5239  axrrecex 5264  letrt 5506  xrletrt 5545  recext 5665  lemul12ait 5806  lemul12itOLD 5807  mulgt1t 5809  ltdivmult 5827  ledivmult 5828  nnrecgt0t 5908  lbreu 6000  nnunb 6025  bndndx 6028  xrub 6035  supxrunb1 6044  lt0nnn0 6071  elnnz1 6110  zeot 6154  uzind 6161  uzwo5OLD 6167  uzwo3lem1 6172  uzwo3lem2 6173  zmax 6176  qbtwnre 6224  qsqueeze 6226  icoshft 6349  fsequb 6463  fsequb2 6464  seqzfveq 6494  expordit 6539  expnbndt 6593  seq1bnd 6855  seq1ublem 6856  cau3ir 6860  faclbnd4lem4 6896  facavgt 6900  fsum1ps 6964  fsumsplit 6966  fsumadd 6968  fsumcom 6974  fsumrev 6975  fsummulc1 6979  fsumcmp 6986  fsumabs 6989  clm4le 7027  2climnn 7047  2climnn0 7048  climaddlem3 7060  climmullem8 7071  climsup 7099  climcau 7100  caucvglem2 7102  caucvglem4 7104  caucvglem6 7106  caucvg 7107  serzf0 7113  ser1f0 7114  ser1cmp2lem 7120  isummulc1 7155  infcvglem3 7166  cvgratlem4 7196  fsum0diag2 7202  fsum0diag4 7204  rescncf 7215  ivthlem7 7230  ivthlem9 7232  ivthlem7OLD 7239  znnenlemOLD 7452  znnen 7453  unbenlem 7455  infxpidmlem7 7509  infxpidmlem8 7510  infxpidmlem12 7514  clsval2 7635  cncnplem4 7727  opnin 7821  metcnp 7839  metcnss2 7851  lmnn 7887  iscau3 7890  iscau4 7892  lmuni 7902  lmsslem 7903  lmle 7911  metcnp4lem2 7919  iscms2lem4 7942  lmcau 7946  cmsss 7947  bcthlem2 7950  bcthlem16 7964  bcthlem17 7965  isgrp 7991  grplactf1o 8049  ubthlem5 8477  ubthlem6 8478  minveclem27 8515  sincosq1lem 8639  sinq12gt0t 8644  normgt0tOLD 8932  normgt0t 8933  hcau2 8994  occon2t 9100  occllem6 9117  projlem26 9150  projlem28 9152  shmods 9300  spansneleq 9432  spansneleqOLD 9433  h1datom 9444  pjjs 9585  hmopidmch 10017  pjnormss 10034  stadd 10111  stm1add3 10112  stadd3 10113  golem2 10137  cvnsymt 10155  dmdmdt 10165  mdslmd1lem1 10189  mdslmd1 10193  mdexch 10199  atcveq0 10212  superpos 10218  hatomistic 10226  atexcht 10245  atoml2 10247  atcvat2 10251  irredlem1 10254  atcvat3 10260  mdsymlem3 10269  mdsymlem5 10271  cdj3lem2b 10298  cdj3 10302  ghomf1olem 10330  homcard 10462  rdmob 10561  cmpmorp 10592  cmphmia 10606  cmphmib 10607  homgrf 10610  ismonc 10620  cmpmon 10621

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

Copyright terms: Public domain