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

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