Theorem sylc 62

Description: A syllogism inference combined with contraction.

Hypotheses

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

Assertion

Ref	Expression
sylc	|- (th -> ch)

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.3	. 2 |- (th -> ps)
2		sylc.2	. . 3 |- (th -> ph)
3		sylc.1	. . 3 |- (ph -> (ps -> ch))
4	2, 3	syl 12	. 2 |- (th -> (ps -> ch))
5	1, 4	mpd 46	1 |- (th -> ch)

Syntax hints:   -> wi 2

This theorem is referenced by:  pm2.65d 117  jc 119  jaod 329  sylanc 361  sbc5g 1450  sbc6g 1451  ssorduni 2249  suceloni 2314  zfrep6 2744  tfrlem12 2960  tfrlem13 2961  oprabval3 3052  th3q 3253  en2d 3303  domnsym 3365  limensuci 3401  unfilem3 3440  inf3lem7 3470  r1val1 3502  ltexpri 3943  prlem936 3949  recexpr 3954  suppr 3957  nngt1ne1t 4440  nngt0t 4441  nnaddm1clt 4452  nn0ltp1let 4556  peano2uz 4602  nn0ind 4612  qbtwnre 4650  ruclem33 4917  ruclem35 4919  his6 5057  norm-it 5080  normpyct 5093  bcs 5101  hlimcaui 5141  occllem6 5185  projlem2 5194  projlem26 5218  projlem27 5219  projlem28 5220  pjthlem10 5234  ococint 5298  osumlem2 5531  osumlem3 5532  osumlem4 5533  pjorth 5559  pjin 5584  stadd3 5689  strlem1 5691  strlem3a 5693  strlem5 5696  jplem1 5701  atcvat3 5774  atcvat4 5775

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

metamath.org