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

Theorem s3eqd 13403
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 13402 . . 3 (𝜑 → ⟨“𝐴𝐵”⟩ = ⟨“𝑁𝑂”⟩)
4 s3eqd.3 . . . 4 (𝜑𝐶 = 𝑃)
54s1eqd 13177 . . 3 (𝜑 → ⟨“𝐶”⟩ = ⟨“𝑃”⟩)
63, 5oveq12d 6542 . 2 (𝜑 → (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩) = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩))
7 df-s3 13388 . 2 ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
8 df-s3 13388 . 2 ⟨“𝑁𝑂𝑃”⟩ = (⟨“𝑁𝑂”⟩ ++ ⟨“𝑃”⟩)
96, 7, 83eqtr4g 2665 1 (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  (class class class)co 6524   ++ cconcat 13091  ⟨“cs1 13092  ⟨“cs2 13380  ⟨“cs3 13381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-ov 6527  df-s1 13100  df-s2 13387  df-s3 13388
This theorem is referenced by:  s4eqd  13404  s3sndisj  13497  s3iunsndisj  13498  tgcgrxfr  25128  ragcgr  25317  perpneq  25324  isperp2  25325  isperp2d  25326  footex  25328  foot  25329  perprag  25333  perpdragALT  25334  colperpexlem1  25337  lmiisolem  25403  hypcgrlem1  25406  hypcgrlem2  25407  trgcopyeu  25413  iscgra  25416  iscgra1  25417  iscgrad  25418  sacgr  25437  isleag  25448  iseqlg  25462  elwwlks2ons3  41158  frgr2wwlk1  41493  fusgr2wsp2nb  41497
  Copyright terms: Public domain W3C validator