Theorem s3eqd

Description: Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypotheses	s2eqd.1	$$⊢\phi \to A=N$$
	s2eqd.2	$$⊢\phi \to B=O$$
	s3eqd.3	$$⊢\phi \to C=P$$
Assertion	s3eqd	$$⊢\phi \to ⟨“ABC”⟩=⟨“NOP”⟩$$

Proof

Step	Hyp	Ref	Expression
1		s2eqd.1	$$⊢\phi \to A=N$$
2		s2eqd.2	$$⊢\phi \to B=O$$
3		s3eqd.3	$$⊢\phi \to C=P$$
4	1 2	s2eqd	$$⊢\phi \to ⟨“AB”⟩=⟨“NO”⟩$$
5	3	s1eqd	$$⊢\phi \to ⟨“C”⟩=⟨“P”⟩$$
6	4 5	oveq12d	$$⊢\phi \to ⟨“AB”⟩\mathrm{++}⟨“C”⟩=⟨“NO”⟩\mathrm{++}⟨“P”⟩$$
7		df-s3	$$⊢⟨“ABC”⟩=⟨“AB”⟩\mathrm{++}⟨“C”⟩$$
8		df-s3	$$⊢⟨“NOP”⟩=⟨“NO”⟩\mathrm{++}⟨“P”⟩$$
9	6 7 8	3eqtr4g	$$⊢\phi \to ⟨“ABC”⟩=⟨“NOP”⟩$$