Theorem s3eq2

Description: Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022)

	Ref	Expression
Assertion	s3eq2	⊢ ( 𝐵 = 𝐷 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ⟨“ 𝐴 𝐷 𝐶 ”⟩ )

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( 𝐵 = 𝐷 → 𝐴 = 𝐴 )
2		id	⊢ ( 𝐵 = 𝐷 → 𝐵 = 𝐷 )
3		eqidd	⊢ ( 𝐵 = 𝐷 → 𝐶 = 𝐶 )
4	1 2 3	s3eqd	⊢ ( 𝐵 = 𝐷 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ = ⟨“ 𝐴 𝐷 𝐶 ”⟩ )