Theorem s6eqd

Description: Equality theorem for a length 6 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$$
Assertion	s6eqd	$$⊢\phi \to ⟨“ABCDEF”⟩=⟨“NOPQRS”⟩$$

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	1 2 3 4 5	s5eqd	$$⊢\phi \to ⟨“ABCDE”⟩=⟨“NOPQR”⟩$$
8	6	s1eqd	$$⊢\phi \to ⟨“F”⟩=⟨“S”⟩$$
9	7 8	oveq12d	$$⊢\phi \to ⟨“ABCDE”⟩\mathrm{++}⟨“F”⟩=⟨“NOPQR”⟩\mathrm{++}⟨“S”⟩$$
10		df-s6	$$⊢⟨“ABCDEF”⟩=⟨“ABCDE”⟩\mathrm{++}⟨“F”⟩$$
11		df-s6	$$⊢⟨“NOPQRS”⟩=⟨“NOPQR”⟩\mathrm{++}⟨“S”⟩$$
12	9 10 11	3eqtr4g	$$⊢\phi \to ⟨“ABCDEF”⟩=⟨“NOPQRS”⟩$$