Theorem cgrtr4and

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

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

Proof

Step	Hyp	Ref	Expression
1		cgrtr4and.1	|- ( ph -> N e. NN )
2		cgrtr4and.2	|- ( ph -> A e. ( EE ` N ) )
3		cgrtr4and.3	|- ( ph -> B e. ( EE ` N ) )
4		cgrtr4and.4	|- ( ph -> C e. ( EE ` N ) )
5		cgrtr4and.5	|- ( ph -> D e. ( EE ` N ) )
6		cgrtr4and.6	|- ( ph -> E e. ( EE ` N ) )
7		cgrtr4and.7	|- ( ph -> F e. ( EE ` N ) )
8		cgrtr4and.8	|- ( ( ph /\ ps ) -> <. A , B >. Cgr <. C , D >. )
9		cgrtr4and.9	|- ( ( ph /\ ps ) -> <. A , B >. Cgr <. E , F >. )
10	1	adantr	|- ( ( ph /\ ps ) -> N e. NN )
11	2	adantr	|- ( ( ph /\ ps ) -> A e. ( EE ` N ) )
12	3	adantr	|- ( ( ph /\ ps ) -> B e. ( EE ` N ) )
13	4	adantr	|- ( ( ph /\ ps ) -> C e. ( EE ` N ) )
14	5	adantr	|- ( ( ph /\ ps ) -> D e. ( EE ` N ) )
15	6	adantr	|- ( ( ph /\ ps ) -> E e. ( EE ` N ) )
16	7	adantr	|- ( ( ph /\ ps ) -> F e. ( EE ` N ) )
17	10 11 12 13 14 15 16 8 9	cgrtr4d	|- ( ( ph /\ ps ) -> <. C , D >. Cgr <. E , F >. )