Metamath Proof Explorer

Theorem cgrid2

Description: Identity law for congruence. (Contributed by Scott Fenton, 12-Jun-2013)

Ref Expression
Assertion cgrid2 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , A >. Cgr <. B , C >. -> B = C ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> N e. NN )
2 simpr1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
3 simpr2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
4 simpr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
5 cgrcom 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ A e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , A >. Cgr <. B , C >. <-> <. B , C >. Cgr <. A , A >. ) )
6 1 2 2 3 4 5 syl122anc 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , A >. Cgr <. B , C >. <-> <. B , C >. Cgr <. A , A >. ) )
7 3anrot 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) <-> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) )
8 axcgrid 
 |-  ( ( N e. NN /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) /\ A e. ( EE ` N ) ) ) -> ( <. B , C >. Cgr <. A , A >. -> B = C ) )
9 7 8 sylan2b 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. B , C >. Cgr <. A , A >. -> B = C ) )
10 6 9 sylbid 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , A >. Cgr <. B , C >. -> B = C ) )