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

Theorem s3eqd 14216
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 14215 . . 3 (𝜑 → ⟨“𝐴𝐵”⟩ = ⟨“𝑁𝑂”⟩)
4 s3eqd.3 . . . 4 (𝜑𝐶 = 𝑃)
54s1eqd 13945 . . 3 (𝜑 → ⟨“𝐶”⟩ = ⟨“𝑃”⟩)
63, 5oveq12d 7166 . 2 (𝜑 → (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩) = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩))
7 df-s3 14201 . 2 ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
8 df-s3 14201 . 2 ⟨“𝑁𝑂𝑃”⟩ = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩)
96, 7, 83eqtr4g 2886 1 (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  (class class class)co 7148   ++ cconcat 13912  ⟨“cs1 13939  ⟨“cs2 14193  ⟨“cs3 14194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6312  df-fv 6360  df-ov 7151  df-s1 13940  df-s2 14200  df-s3 14201
This theorem is referenced by:  s4eqd  14217  s3eq2  14222  s3sndisj  14317  s3iunsndisj  14318  ragcgr  26407  perpneq  26414  isperp2  26415  isperp2d  26416  footexALT  26418  footexlem2  26420  foot  26422  perprag  26426  perpdragALT  26427  colperpexlem1  26430  lmiisolem  26496  hypcgrlem1  26499  hypcgrlem2  26500  trgcopyeu  26506  iscgra  26509  iscgra1  26510  iscgrad  26511  sacgr  26531  isleag  26547  isleagd  26548  iseqlg  26567
  Copyright terms: Public domain W3C validator