Theorem cgrcomland

Description: Deduction form of cgrcoml . (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	cgrcomland	|- ( ( ph /\ ps ) -> <. B , A >. Cgr <. C , D >. )

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		cgrcoml	|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. A , B >. Cgr <. C , D >. <-> <. B , A >. Cgr <. C , D >. ) )
8	1 2 3 4 5 7	syl122anc	|- ( ph -> ( <. A , B >. Cgr <. C , D >. <-> <. B , A >. Cgr <. C , D >. ) )
9	8	adantr	|- ( ( ph /\ ps ) -> ( <. A , B >. Cgr <. C , D >. <-> <. B , A >. Cgr <. C , D >. ) )
10	6 9	mpbid	|- ( ( ph /\ ps ) -> <. B , A >. Cgr <. C , D >. )