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 ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( 𝐴 = 𝐷𝐵 = 𝐸𝐶 = 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 s3eqs2s1eq ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐶 ”⟩ = ⟨“ 𝐹 ”⟩ ) ) )
2 3simpa ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) → ( 𝐴𝑉𝐵𝑉 ) )
3 3simpa ( ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) → ( 𝐷𝑉𝐸𝑉 ) )
4 s2eq2seq ( ( ( 𝐴𝑉𝐵𝑉 ) ∧ ( 𝐷𝑉𝐸𝑉 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐷 𝐸 ”⟩ ↔ ( 𝐴 = 𝐷𝐵 = 𝐸 ) ) )
5 2 3 4 syl2an ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) ) → ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐷 𝐸 ”⟩ ↔ ( 𝐴 = 𝐷𝐵 = 𝐸 ) ) )
6 simp3 ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) → 𝐶𝑉 )
7 simp3 ( ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) → 𝐹𝑉 )
8 s111 ( ( 𝐶𝑉𝐹𝑉 ) → ( ⟨“ 𝐶 ”⟩ = ⟨“ 𝐹 ”⟩ ↔ 𝐶 = 𝐹 ) )
9 6 7 8 syl2an ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) ) → ( ⟨“ 𝐶 ”⟩ = ⟨“ 𝐹 ”⟩ ↔ 𝐶 = 𝐹 ) )
10 5 9 anbi12d ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) ) → ( ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐶 ”⟩ = ⟨“ 𝐹 ”⟩ ) ↔ ( ( 𝐴 = 𝐷𝐵 = 𝐸 ) ∧ 𝐶 = 𝐹 ) ) )
11 df-3an ( ( 𝐴 = 𝐷𝐵 = 𝐸𝐶 = 𝐹 ) ↔ ( ( 𝐴 = 𝐷𝐵 = 𝐸 ) ∧ 𝐶 = 𝐹 ) )
12 10 11 bitr4di ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) ) → ( ( ⟨“ 𝐴 𝐵 ”⟩ = ⟨“ 𝐷 𝐸 ”⟩ ∧ ⟨“ 𝐶 ”⟩ = ⟨“ 𝐹 ”⟩ ) ↔ ( 𝐴 = 𝐷𝐵 = 𝐸𝐶 = 𝐹 ) ) )
13 1 12 bitrd ( ( ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ∧ ( 𝐷𝑉𝐸𝑉𝐹𝑉 ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ( 𝐴 = 𝐷𝐵 = 𝐸𝐶 = 𝐹 ) ) )