Theorem syl6c 70

Description: Inference combining syl6 35 with contraction. (Contributed by Alan Sare, 2-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
syl6c	|- ( ph -> ( ps -> ta ) )

Proof of Theorem syl6c

Step	Hyp	Ref	Expression
1		syl6c.2	. 2 |- ( ph -> ( ps -> th ) )
2		syl6c.1	. . 3 |- ( ph -> ( ps -> ch ) )
3		syl6c.3	. . 3 |- ( ch -> ( th -> ta ) )
4	2, 3	syl6 35	. 2 |- ( ph -> ( ps -> ( th -> ta ) ) )
5	1, 4	mpdd 43	1 |- ( ph -> ( ps -> ta ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  syl6ci  71  syldd  72  impbidd  200  pm5.21ndd  369  jcad  555  zorn2lem6  9323  sqreulem  14099  ontopbas  32427  ontgval  32430  ordtoplem  32434  ordcmp  32446  ee33  38727  sb5ALT  38731  tratrb  38746  onfrALTlem2  38761  onfrALT  38764  ax6e2ndeq  38775  ee22an  38898  sspwtrALT  39049  sspwtrALT2  39058  trintALT  39117