Theorem cgrcomand

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

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

Proof

Step	Hyp	Ref	Expression
1		cgrcomand.1	|- ( ph -> N e. NN )
2		cgrcomand.2	|- ( ph -> A e. ( EE ` N ) )
3		cgrcomand.3	|- ( ph -> B e. ( EE ` N ) )
4		cgrcomand.4	|- ( ph -> C e. ( EE ` N ) )
5		cgrcomand.5	|- ( ph -> D e. ( EE ` N ) )
6		cgrcomand.6	|- ( ( ph /\ ps ) -> <. A , B >. Cgr <. C , D >. )
7		cgrcom	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , D >. <-> <. C , D >. Cgr <. A , B >. ) )
8	1 2 3 4 5 7	syl122anc	|- ( ph -> ( <. A , B >. Cgr <. C , D >. <-> <. C , D >. Cgr <. A , B >. ) )
9	8	adantr	|- ( ( ph /\ ps ) -> ( <. A , B >. Cgr <. C , D >. <-> <. C , D >. Cgr <. A , B >. ) )
10	6 9	mpbid	|- ( ( ph /\ ps ) -> <. C , D >. Cgr <. A , B >. )