Theorem s3eqd 14773

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 14772	. . 3 ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ = ⟨“𝑁𝑂”⟩)
4		s3eqd.3	. . . 4 ⊢ (𝜑 → 𝐶 = 𝑃)
5	4	s1eqd 14511	. . 3 ⊢ (𝜑 → ⟨“𝐶”⟩ = ⟨“𝑃”⟩)
6	3, 5	oveq12d 7370	. 2 ⊢ (𝜑 → (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩) = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩))
7		df-s3 14758	. 2 ⊢ ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
8		df-s3 14758	. 2 ⊢ ⟨“𝑁𝑂𝑃”⟩ = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩)
9	6, 7, 8	3eqtr4g 2793	1 ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)

Syntax hints:   → wi 4   = wceq 1541  (class class class)co 7352   ++ cconcat 14479  ⟨“cs1 14505  ⟨“cs2 14750  ⟨“cs3 14751

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-s1 14506  df-s2 14757  df-s3 14758

This theorem is referenced by:  s4eqd  14774  s3eq2  14779  s3sndisj  14876  s3iunsndisj  14877  ragcgr  28686  perpneq  28693  isperp2  28694  isperp2d  28695  footexALT  28697  footexlem2  28699  foot  28701  perprag  28705  perpdragALT  28706  colperpexlem1  28709  lmiisolem  28775  hypcgrlem1  28778  hypcgrlem2  28779  trgcopyeu  28785  iscgra  28788  iscgra1  28789  iscgrad  28790  sacgr  28810  isleag  28826  isleagd  28827  iseqlg  28846