Theorem s5eqd

Description: Equality theorem for a length 5 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$$
Assertion	s5eqd	$$⊢\phi \to ⟨“ABCDE”⟩=⟨“NOPQR”⟩$$

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	1 2 3 4	s4eqd	$$⊢\phi \to ⟨“ABCD”⟩=⟨“NOPQ”⟩$$
7	5	s1eqd	$$⊢\phi \to ⟨“E”⟩=⟨“R”⟩$$
8	6 7	oveq12d	$$⊢\phi \to ⟨“ABCD”⟩\mathrm{++}⟨“E”⟩=⟨“NOPQ”⟩\mathrm{++}⟨“R”⟩$$
9		df-s5	$$⊢⟨“ABCDE”⟩=⟨“ABCD”⟩\mathrm{++}⟨“E”⟩$$
10		df-s5	$$⊢⟨“NOPQR”⟩=⟨“NOPQ”⟩\mathrm{++}⟨“R”⟩$$
11	8 9 10	3eqtr4g	$$⊢\phi \to ⟨“ABCDE”⟩=⟨“NOPQR”⟩$$