Theorem cgrtr4d

Description: Deduction form of axcgrtr . (Contributed by Scott Fenton, 13-Oct-2013)

	Ref	Expression
Hypotheses	cgrtr4d.1	|- ( ph -> N e. NN )
	cgrtr4d.2	|- ( ph -> A e. ( EE ` N ) )
	cgrtr4d.3	|- ( ph -> B e. ( EE ` N ) )
	cgrtr4d.4	|- ( ph -> C e. ( EE ` N ) )
	cgrtr4d.5	|- ( ph -> D e. ( EE ` N ) )
	cgrtr4d.6	|- ( ph -> E e. ( EE ` N ) )
	cgrtr4d.7	|- ( ph -> F e. ( EE ` N ) )
	cgrtr4d.8	|- ( ph -> <. A , B >. Cgr <. C , D >. )
	cgrtr4d.9	|- ( ph -> <. A , B >. Cgr <. E , F >. )
Assertion	cgrtr4d	|- ( ph -> <. C , D >. Cgr <. E , F >. )

Proof

Step	Hyp	Ref	Expression
1		cgrtr4d.1	|- ( ph -> N e. NN )
2		cgrtr4d.2	|- ( ph -> A e. ( EE ` N ) )
3		cgrtr4d.3	|- ( ph -> B e. ( EE ` N ) )
4		cgrtr4d.4	|- ( ph -> C e. ( EE ` N ) )
5		cgrtr4d.5	|- ( ph -> D e. ( EE ` N ) )
6		cgrtr4d.6	|- ( ph -> E e. ( EE ` N ) )
7		cgrtr4d.7	|- ( ph -> F e. ( EE ` N ) )
8		cgrtr4d.8	|- ( ph -> <. A , B >. Cgr <. C , D >. )
9		cgrtr4d.9	|- ( ph -> <. A , B >. Cgr <. E , F >. )
10		axcgrtr	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. C , D >. /\ <. A , B >. Cgr <. E , F >. ) -> <. C , D >. Cgr <. E , F >. ) )
11	1 2 3 4 5 6 7 10	syl133anc	|- ( ph -> ( ( <. A , B >. Cgr <. C , D >. /\ <. A , B >. Cgr <. E , F >. ) -> <. C , D >. Cgr <. E , F >. ) )
12	8 9 11	mp2and	|- ( ph -> <. C , D >. Cgr <. E , F >. )