Theorem s3eq2

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

	Ref	Expression
Assertion	s3eq2	$$⊢B=D\to ⟨“ABC”⟩=⟨“ADC”⟩$$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢B=D\to A=A$$
2		id	$$⊢B=D\to B=D$$
3		eqidd	$$⊢B=D\to C=C$$
4	1 2 3	s3eqd	$$⊢B=D\to ⟨“ABC”⟩=⟨“ADC”⟩$$