Metamath Proof Explorer

Theorem cgrtr3

Description: Transitivity law for congruence. (Contributed by Scott Fenton, 7-Oct-2013)

Ref

Expression

Assertion

|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. E , F >. ) -> <. A , B >. Cgr <. C , D >. ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> N e. NN )
2		simp21	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
3		simp22	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
4		simp32	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> E e. ( EE ` N ) )
5		simp33	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> F e. ( EE ` N ) )
6		simp23	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
7		simp31	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> D e. ( EE ` N ) )
8		simprl	\|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. E , F >. ) ) -> <. A , B >. Cgr <. E , F >. )
9		simprr	\|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. E , F >. ) ) -> <. C , D >. Cgr <. E , F >. )
10	1 6 7 4 5 9	cgrcomand	\|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. E , F >. ) ) -> <. E , F >. Cgr <. C , D >. )
11	1 2 3 4 5 6 7 8 10	cgrtrand	\|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) /\ ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. E , F >. ) ) -> <. A , B >. Cgr <. C , D >. )
12	11	ex	\|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) /\ ( D e. ( EE ` N ) /\ E e. ( EE ` N ) /\ F e. ( EE ` N ) ) ) -> ( ( <. A , B >. Cgr <. E , F >. /\ <. C , D >. Cgr <. E , F >. ) -> <. A , B >. Cgr <. C , D >. ) )