Step |
Hyp |
Ref |
Expression |
1 |
|
cgrcomim |
|- ( ( 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 >. ) ) |
2 |
|
cgrcomim |
|- ( ( N e. NN /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( <. C , D >. Cgr <. A , B >. -> <. A , B >. Cgr <. C , D >. ) ) |
3 |
2
|
3com23 |
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ D e. ( EE ` N ) ) ) -> ( <. C , D >. Cgr <. A , B >. -> <. A , B >. Cgr <. C , D >. ) ) |
4 |
1 3
|
impbid |
|- ( ( 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 >. ) ) |