Theorem s3eqd 14768

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

Hypotheses

Ref	Expression
s2eqd.1	⊢ (𝜑 → 𝐴 = 𝑁)
s2eqd.2	⊢ (𝜑 → 𝐵 = 𝑂)
s3eqd.3	⊢ (𝜑 → 𝐶 = 𝑃)

Assertion

Ref	Expression
s3eqd	⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)

Proof of Theorem s3eqd

Step	Hyp	Ref	Expression
1		s2eqd.1	. . . 4 ⊢ (𝜑 → 𝐴 = 𝑁)
2		s2eqd.2	. . . 4 ⊢ (𝜑 → 𝐵 = 𝑂)
3	1, 2	s2eqd 14767	. . 3 ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ = ⟨“𝑁𝑂”⟩)
4		s3eqd.3	. . . 4 ⊢ (𝜑 → 𝐶 = 𝑃)
5	4	s1eqd 14506	. . 3 ⊢ (𝜑 → ⟨“𝐶”⟩ = ⟨“𝑃”⟩)
6	3, 5	oveq12d 7364	. 2 ⊢ (𝜑 → (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩) = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩))
7		df-s3 14753	. 2 ⊢ ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
8		df-s3 14753	. 2 ⊢ ⟨“𝑁𝑂𝑃”⟩ = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩)
9	6, 7, 8	3eqtr4g 2791	1 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)

Syntax hints:   → wi 4   = wceq 1541  (class class class)co 7346   ++ cconcat 14474  ⟨“cs1 14500  ⟨“cs2 14745  ⟨“cs3 14746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349  df-s1 14501  df-s2 14752  df-s3 14753

This theorem is referenced by:  s4eqd  14769  s3eq2  14774  s3sndisj  14871  s3iunsndisj  14872  ragcgr  28683  perpneq  28690  isperp2  28691  isperp2d  28692  footexALT  28694  footexlem2  28696  foot  28698  perprag  28702  perpdragALT  28703  colperpexlem1  28706  lmiisolem  28772  hypcgrlem1  28775  hypcgrlem2  28776  trgcopyeu  28782  iscgra  28785  iscgra1  28786  iscgrad  28787  sacgr  28807  isleag  28823  isleagd  28824  iseqlg  28843