Theorem syld 27

Description: Syllogism deduction. (The proof was shortened by Mel L. O'Cat, 7-Aug-04.)

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	. . . 4 |- (ph -> (ch -> th))
3	2	syl3d 26	. . 3 |- (ph -> ((ps -> ch) -> (ps -> th)))
4	3	a2i 8	. 2 |- ((ph -> (ps -> ch)) -> (ph -> (ps -> th)))
5	1, 4	ax-mp 6	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 2

This theorem is referenced by:  syl34d 29  sylcom 51  syl5d 53  syl6d 54  sylibd 177  sylbid 178  sylibrd 179  sylbird 180  syland 352  sylan9 359  del34 835  del35 836  cbv1 845  sb6y 872  hbsb3 875  sbequi 876  sbn1 880  sbied 903  hbsb4 905  sb9i 920  ralcom2 1314  trel3 2049  wefrc 2195  ordelord 2221  oninton 2267  orduniorsuc 2337  tfindsg 2402  funun 2700  fnex 2740  fvopab3ig 2869  isomin 2937  isofrlem 2939  tfrlem9 2957  abianfp 3000  oprabvalig 3048  oaordi 3148  nnmordi 3188  ecopoprtrn 3247  f1oeng 3298  f1domg 3299  onomeneq 3414  pssnn 3428  unblem3 3433  isfinite2 3437  unfi 3441  inf3lem3 3466  inf3lem5 3468  r1tr 3498  rankr1 3518  rankval3 3525  zornlem2 3604  zornlem3 3605  imadomg 3616  carduni 3664  alephle 3689  cardaleph 3690  iscard3 3693  axacndlem4 3756  addnidpi 3822  ordpipq 3850  ltbtwnpq 3878  genpnnp 3902  addclprlem1 3912  addclprlem2 3913  mulclprlem 3915  distrlem1pr 3921  distrlem2pr 3922  distrlem4pr 3924  psslinpr 3929  ltaddpr2 3935  ltexprlem6 3941  ltexpri 3943  addcanpr 3946  suplem2pr 3956  ltsrpr 3980  mulgt0sr 4008  recexsr 4010  suppsrlem 4015  suprelem 4053  axrecex 4079  axrrecex 4081  letrt 4291  ledivt 4405  ltdivmult 4408  nnrecgt0t 4447  nnunb 4520  lt0nnn0 4549  elnnz1 4581  uzwo3lem1 4614  uzwo3lem2 4615  qbtwnre 4650  znnenlem 4929  znnen 4930  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem12 4944  normgt0t 5078  shsubclt 5125  occon2t 5169  occllem6 5185  projlem26 5218  projlem28 5220  shintcl 5294  shmods 5363  spansneleq 5475  h1datom 5483  pjnormss 5638  stadd 5687  stm1add3 5688  stadd3 5689  golem2 5705  cvnsymt 5722  cvntrt 5724  dmdbr 5731  atcveq0 5746  hatomistic 5755  atexch 5769  atcvat2 5772  atcvat3 5774  mdsymlem3 5778  mdsymlem5 5780

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org