Metamath Proof Explorer

Theorem cgr3rflx

Description: Identity law for three-place congruence. (Contributed by Scott Fenton, 6-Oct-2013)

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

Proof

Step Hyp Ref Expression
1 cgrrflx 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. Cgr <. A , B >. )
2 1 3adant3r3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> <. A , B >. Cgr <. A , B >. )
3 cgrrflx 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> <. A , C >. Cgr <. A , C >. )
4 3 3adant3r2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> <. A , C >. Cgr <. A , C >. )
5 cgrrflx 
 |-  ( ( N e. NN /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> <. B , C >. Cgr <. B , C >. )
6 5 3adant3r1 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> <. B , C >. Cgr <. B , C >. )
7 brcgr3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. <-> ( <. A , B >. Cgr <. A , B >. /\ <. A , C >. Cgr <. A , C >. /\ <. B , C >. Cgr <. B , C >. ) ) )
8 7 3anidm23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. <-> ( <. A , B >. Cgr <. A , B >. /\ <. A , C >. Cgr <. A , C >. /\ <. B , C >. Cgr <. B , C >. ) ) )
9 2 4 6 8 mpbir3and 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> <. A , <. B , C >. >. Cgr3 <. A , <. B , C >. >. )