Theorem s3eq3seq

Description: Two length 3 words are equal iff the corresponding symbols are equal. (Contributed by AV, 4-Jan-2022)

	Ref	Expression
Assertion	s3eq3seq	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B C "> = <" D E F "> <-> ( A = D /\ B = E /\ C = F ) ) )

Proof

Step	Hyp	Ref	Expression
1		s3eqs2s1eq	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B C "> = <" D E F "> <-> ( <" A B "> = <" D E "> /\ <" C "> = <" F "> ) ) )
2		3simpa	|- ( ( A e. V /\ B e. V /\ C e. V ) -> ( A e. V /\ B e. V ) )
3		3simpa	|- ( ( D e. V /\ E e. V /\ F e. V ) -> ( D e. V /\ E e. V ) )
4		s2eq2seq	|- ( ( ( A e. V /\ B e. V ) /\ ( D e. V /\ E e. V ) ) -> ( <" A B "> = <" D E "> <-> ( A = D /\ B = E ) ) )
5	2 3 4	syl2an	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B "> = <" D E "> <-> ( A = D /\ B = E ) ) )
6		simp3	|- ( ( A e. V /\ B e. V /\ C e. V ) -> C e. V )
7		simp3	|- ( ( D e. V /\ E e. V /\ F e. V ) -> F e. V )
8		s111	|- ( ( C e. V /\ F e. V ) -> ( <" C "> = <" F "> <-> C = F ) )
9	6 7 8	syl2an	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" C "> = <" F "> <-> C = F ) )
10	5 9	anbi12d	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( ( <" A B "> = <" D E "> /\ <" C "> = <" F "> ) <-> ( ( A = D /\ B = E ) /\ C = F ) ) )
11		df-3an	|- ( ( A = D /\ B = E /\ C = F ) <-> ( ( A = D /\ B = E ) /\ C = F ) )
12	10 11	bitr4di	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( ( <" A B "> = <" D E "> /\ <" C "> = <" F "> ) <-> ( A = D /\ B = E /\ C = F ) ) )
13	1 12	bitrd	|- ( ( ( A e. V /\ B e. V /\ C e. V ) /\ ( D e. V /\ E e. V /\ F e. V ) ) -> ( <" A B C "> = <" D E F "> <-> ( A = D /\ B = E /\ C = F ) ) )