Theorem s3eqd 13985

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

Syntax hints:   → wi 4   = wceq 1656  (class class class)co 6905   ++ cconcat 13630  ⟨“cs1 13655  ⟨“cs2 13962  ⟨“cs3 13963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-iota 6086  df-fv 6131  df-ov 6908  df-s1 13656  df-s2 13969  df-s3 13970

This theorem is referenced by:  s4eqd  13986  s3eq2  13991  s3sndisj  14085  s3iunsndisj  14086  tgcgrxfr  25830  ragcgr  26019  perpneq  26026  isperp2  26027  isperp2d  26028  footex  26030  foot  26031  perprag  26035  perpdragALT  26036  colperpexlem1  26039  lmiisolem  26105  hypcgrlem1  26108  hypcgrlem2  26109  trgcopyeu  26115  iscgra  26118  iscgra1  26119  iscgrad  26120  sacgr  26139  sacgrOLD  26140  isleag  26151  iseqlg  26166