Theorem s4eqd

Description: Equality theorem for a length 4 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$$
Assertion	s4eqd	$$⊢\phi \to ⟨“ABCD”⟩=⟨“NOPQ”⟩$$

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	1 2 3	s3eqd	$$⊢\phi \to ⟨“ABC”⟩=⟨“NOP”⟩$$
6	4	s1eqd	$$⊢\phi \to ⟨“D”⟩=⟨“Q”⟩$$
7	5 6	oveq12d	$$⊢\phi \to ⟨“ABC”⟩\mathrm{++}⟨“D”⟩=⟨“NOP”⟩\mathrm{++}⟨“Q”⟩$$
8		df-s4	$$⊢⟨“ABCD”⟩=⟨“ABC”⟩\mathrm{++}⟨“D”⟩$$
9		df-s4	$$⊢⟨“NOPQ”⟩=⟨“NOP”⟩\mathrm{++}⟨“Q”⟩$$
10	7 8 9	3eqtr4g	$$⊢\phi \to ⟨“ABCD”⟩=⟨“NOPQ”⟩$$