Theorem syl6c 64

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

Hypotheses

Ref	Expression
syl6c.1
syl6c.2
syl6c.3

Assertion

Ref	Expression
syl6c

Proof of Theorem syl6c

Step	Hyp	Ref	Expression
1		syl6c.2	. 2
2		syl6c.1	. . 3
3		syl6c.3	. . 3
4	2, 3	syl6 33	. 2
5	1, 4	mpdd 40	1

Syntax hints:  ->wi 4

This theorem is referenced by:  syl6ci  65  syldd  66  impbidd  189  pm5.21ndd  354  jcad  533  zorn2lem6  8902  sqreulem  13192  ontopbas  29893  ontgval  29896  ordtoplem  29900  ordcmp  29912  ee33  33291  sb5ALT  33295  tratrb  33307  onfrALTlem2  33318  onfrALT  33321  ax6e2ndeq  33332  ee22an  33459  sspwtrALT  33620  sspwtrALT2  33623  trintALT  33681

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