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 ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V → ⟨“ ABC ”⟩ = ⟨“ DEF ”⟩ ↔ A = D ∧ B = E ∧ C = F

Proof

Step Hyp Ref Expression
1 s3eqs2s1eq ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V → ⟨“ ABC ”⟩ = ⟨“ DEF ”⟩ ↔ ⟨“ AB ”⟩ = ⟨“ DE ”⟩ ∧ ⟨“ C ”⟩ = ⟨“ F ”⟩
2 3simpa ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V ∧ B ∈ V
3 3simpa ⊢ D ∈ V ∧ E ∈ V ∧ F ∈ V → D ∈ V ∧ E ∈ V
4 s2eq2seq ⊢ A ∈ V ∧ B ∈ V ∧ D ∈ V ∧ E ∈ V → ⟨“ AB ”⟩ = ⟨“ DE ”⟩ ↔ A = D ∧ B = E
5 2 3 4 syl2an ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V → ⟨“ AB ”⟩ = ⟨“ DE ”⟩ ↔ A = D ∧ B = E
6 simp3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V
7 simp3 ⊢ D ∈ V ∧ E ∈ V ∧ F ∈ V → F ∈ V
8 s111 ⊢ C ∈ V ∧ F ∈ V → ⟨“ C ”⟩ = ⟨“ F ”⟩ ↔ C = F
9 6 7 8 syl2an ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V → ⟨“ C ”⟩ = ⟨“ F ”⟩ ↔ C = F
10 5 9 anbi12d ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V → ⟨“ AB ”⟩ = ⟨“ DE ”⟩ ∧ ⟨“ 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 ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V → ⟨“ AB ”⟩ = ⟨“ DE ”⟩ ∧ ⟨“ C ”⟩ = ⟨“ F ”⟩ ↔ A = D ∧ B = E ∧ C = F
13 1 12 bitrd ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V ∧ E ∈ V ∧ F ∈ V → ⟨“ ABC ”⟩ = ⟨“ DEF ”⟩ ↔ A = D ∧ B = E ∧ C = F