MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  s3eqd Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 s2eqd.1 . . . 4 (𝜑𝐴 = 𝑁)
2 s2eqd.2 . . . 4 (𝜑𝐵 = 𝑂)
31, 2s2eqd 13984 . . 3 (𝜑 → ⟨“𝐴𝐵”⟩ = ⟨“𝑁𝑂”⟩)
4 s3eqd.3 . . . 4 (𝜑𝐶 = 𝑃)
54s1eqd 13661 . . 3 (𝜑 → ⟨“𝐶”⟩ = ⟨“𝑃”⟩)
63, 5oveq12d 6923 . 2 (𝜑 → (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩) = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩))
7 df-s3 13970 . 2 ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
8 df-s3 13970 . 2 ⟨“𝑁𝑂𝑃”⟩ = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩)
96, 7, 83eqtr4g 2886 1 (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator