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

Theorem s3eqd 14903
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 14902 . . 3 (𝜑 → ⟨“𝐴𝐵”⟩ = ⟨“𝑁𝑂”⟩)
4 s3eqd.3 . . . 4 (𝜑𝐶 = 𝑃)
54s1eqd 14639 . . 3 (𝜑 → ⟨“𝐶”⟩ = ⟨“𝑃”⟩)
63, 5oveq12d 7449 . 2 (𝜑 → (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩) = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩))
7 df-s3 14888 . 2 ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
8 df-s3 14888 . 2 ⟨“𝑁𝑂𝑃”⟩ = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩)
96, 7, 83eqtr4g 2802 1 (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  (class class class)co 7431   ++ cconcat 14608  ⟨“cs1 14633  ⟨“cs2 14880  ⟨“cs3 14881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-s1 14634  df-s2 14887  df-s3 14888
This theorem is referenced by:  s4eqd  14904  s3eq2  14909  s3sndisj  15006  s3iunsndisj  15007  ragcgr  28715  perpneq  28722  isperp2  28723  isperp2d  28724  footexALT  28726  footexlem2  28728  foot  28730  perprag  28734  perpdragALT  28735  colperpexlem1  28738  lmiisolem  28804  hypcgrlem1  28807  hypcgrlem2  28808  trgcopyeu  28814  iscgra  28817  iscgra1  28818  iscgrad  28819  sacgr  28839  isleag  28855  isleagd  28856  iseqlg  28875
  Copyright terms: Public domain W3C validator