Theorem cgrtr3and

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

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

Proof

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