Theorem s7eqd

Description: Equality theorem for a length 7 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$$
Assertion	s7eqd	$$⊢\phi \to ⟨“ABCDEFG”⟩=⟨“NOPQRST”⟩$$

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	1 2 3 4 5 6	s6eqd	$$⊢\phi \to ⟨“ABCDEF”⟩=⟨“NOPQRS”⟩$$
9	7	s1eqd	$$⊢\phi \to ⟨“G”⟩=⟨“T”⟩$$
10	8 9	oveq12d	$$⊢\phi \to ⟨“ABCDEF”⟩\mathrm{++}⟨“G”⟩=⟨“NOPQRS”⟩\mathrm{++}⟨“T”⟩$$
11		df-s7	$$⊢⟨“ABCDEFG”⟩=⟨“ABCDEF”⟩\mathrm{++}⟨“G”⟩$$
12		df-s7	$$⊢⟨“NOPQRST”⟩=⟨“NOPQRS”⟩\mathrm{++}⟨“T”⟩$$
13	10 11 12	3eqtr4g	$$⊢\phi \to ⟨“ABCDEFG”⟩=⟨“NOPQRST”⟩$$