Theorem s8eqd

Description: Equality theorem for a length 8 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$$
	s4eqd.4	$$⊢\phi \to D=Q$$
	s5eqd.5	$$⊢\phi \to E=R$$
	s6eqd.6	$$⊢\phi \to F=S$$
	s7eqd.6	$$⊢\phi \to G=T$$
	s8eqd.6	$$⊢\phi \to H=U$$
Assertion	s8eqd	$$⊢\phi \to ⟨“ABCDEFGH”⟩=⟨“NOPQRSTU”⟩$$

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		s4eqd.4	$$⊢\phi \to D=Q$$
5		s5eqd.5	$$⊢\phi \to E=R$$
6		s6eqd.6	$$⊢\phi \to F=S$$
7		s7eqd.6	$$⊢\phi \to G=T$$
8		s8eqd.6	$$⊢\phi \to H=U$$
9	1 2 3 4 5 6 7	s7eqd	$$⊢\phi \to ⟨“ABCDEFG”⟩=⟨“NOPQRST”⟩$$
10	8	s1eqd	$$⊢\phi \to ⟨“H”⟩=⟨“U”⟩$$
11	9 10	oveq12d	$$⊢\phi \to ⟨“ABCDEFG”⟩\mathrm{++}⟨“H”⟩=⟨“NOPQRST”⟩\mathrm{++}⟨“U”⟩$$
12		df-s8	$$⊢⟨“ABCDEFGH”⟩=⟨“ABCDEFG”⟩\mathrm{++}⟨“H”⟩$$
13		df-s8	$$⊢⟨“NOPQRSTU”⟩=⟨“NOPQRST”⟩\mathrm{++}⟨“U”⟩$$
14	11 12 13	3eqtr4g	$$⊢\phi \to ⟨“ABCDEFGH”⟩=⟨“NOPQRSTU”⟩$$