![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > s3eqd | Structured version Visualization version GIF version |
Description: Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
Ref | Expression |
---|---|
s2eqd.1 | ⊢ (𝜑 → 𝐴 = 𝑁) |
s2eqd.2 | ⊢ (𝜑 → 𝐵 = 𝑂) |
s3eqd.3 | ⊢ (𝜑 → 𝐶 = 𝑃) |
Ref | Expression |
---|---|
s3eqd | ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 = 〈“𝑁𝑂𝑃”〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | s2eqd.1 | . . . 4 ⊢ (𝜑 → 𝐴 = 𝑁) | |
2 | s2eqd.2 | . . . 4 ⊢ (𝜑 → 𝐵 = 𝑂) | |
3 | 1, 2 | s2eqd 14216 | . . 3 ⊢ (𝜑 → 〈“𝐴𝐵”〉 = 〈“𝑁𝑂”〉) |
4 | s3eqd.3 | . . . 4 ⊢ (𝜑 → 𝐶 = 𝑃) | |
5 | 4 | s1eqd 13946 | . . 3 ⊢ (𝜑 → 〈“𝐶”〉 = 〈“𝑃”〉) |
6 | 3, 5 | oveq12d 7153 | . 2 ⊢ (𝜑 → (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) = (〈“𝑁𝑂”〉 ++ 〈“𝑃”〉)) |
7 | df-s3 14202 | . 2 ⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) | |
8 | df-s3 14202 | . 2 ⊢ 〈“𝑁𝑂𝑃”〉 = (〈“𝑁𝑂”〉 ++ 〈“𝑃”〉) | |
9 | 6, 7, 8 | 3eqtr4g 2858 | 1 ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 = 〈“𝑁𝑂𝑃”〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 (class class class)co 7135 ++ cconcat 13913 〈“cs1 13940 〈“cs2 14194 〈“cs3 14195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-iota 6283 df-fv 6332 df-ov 7138 df-s1 13941 df-s2 14201 df-s3 14202 |
This theorem is referenced by: s4eqd 14218 s3eq2 14223 s3sndisj 14318 s3iunsndisj 14319 ragcgr 26501 perpneq 26508 isperp2 26509 isperp2d 26510 footexALT 26512 footexlem2 26514 foot 26516 perprag 26520 perpdragALT 26521 colperpexlem1 26524 lmiisolem 26590 hypcgrlem1 26593 hypcgrlem2 26594 trgcopyeu 26600 iscgra 26603 iscgra1 26604 iscgrad 26605 sacgr 26625 isleag 26641 isleagd 26642 iseqlg 26661 |
Copyright terms: Public domain | W3C validator |