Theorem cgrcomlrand

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

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

Proof

Step	Hyp	Ref	Expression
1		cgrcomlrand.1	|- ( ph -> N e. NN )
2		cgrcomlrand.2	|- ( ph -> A e. ( EE ` N ) )
3		cgrcomlrand.3	|- ( ph -> B e. ( EE ` N ) )
4		cgrcomlrand.4	|- ( ph -> C e. ( EE ` N ) )
5		cgrcomlrand.5	|- ( ph -> D e. ( EE ` N ) )
6		cgrcomlrand.6	|- ( ( ph /\ ps ) -> <. A , B >. Cgr <. C , D >. )
7	1 2 3 4 5 6	cgrcomrand	|- ( ( ph /\ ps ) -> <. A , B >. Cgr <. D , C >. )
8	1 2 3 5 4 7	cgrcomland	|- ( ( ph /\ ps ) -> <. B , A >. Cgr <. D , C >. )