This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )