Theorem s2eqd

Description: Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypotheses	s2eqd.1	$$⊢\phi \to A=N$$
	s2eqd.2	$$⊢\phi \to B=O$$
Assertion	s2eqd	$$⊢\phi \to ⟨“AB”⟩=⟨“NO”⟩$$

Proof

Step	Hyp	Ref	Expression
1		s2eqd.1	$$⊢\phi \to A=N$$
2		s2eqd.2	$$⊢\phi \to B=O$$
3	1	s1eqd	$$⊢\phi \to ⟨“A”⟩=⟨“N”⟩$$
4	2	s1eqd	$$⊢\phi \to ⟨“B”⟩=⟨“O”⟩$$
5	3 4	oveq12d	$$⊢\phi \to ⟨“A”⟩\mathrm{++}⟨“B”⟩=⟨“N”⟩\mathrm{++}⟨“O”⟩$$
6		df-s2	$$⊢⟨“AB”⟩=⟨“A”⟩\mathrm{++}⟨“B”⟩$$
7		df-s2	$$⊢⟨“NO”⟩=⟨“N”⟩\mathrm{++}⟨“O”⟩$$
8	5 6 7	3eqtr4g	$$⊢\phi \to ⟨“AB”⟩=⟨“NO”⟩$$