![]() |
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 13984 | . . 3 ⊢ (𝜑 → 〈“𝐴𝐵”〉 = 〈“𝑁𝑂”〉) |
4 | s3eqd.3 | . . . 4 ⊢ (𝜑 → 𝐶 = 𝑃) | |
5 | 4 | s1eqd 13661 | . . 3 ⊢ (𝜑 → 〈“𝐶”〉 = 〈“𝑃”〉) |
6 | 3, 5 | oveq12d 6923 | . 2 ⊢ (𝜑 → (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) = (〈“𝑁𝑂”〉 ++ 〈“𝑃”〉)) |
7 | df-s3 13970 | . 2 ⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) | |
8 | df-s3 13970 | . 2 ⊢ 〈“𝑁𝑂𝑃”〉 = (〈“𝑁𝑂”〉 ++ 〈“𝑃”〉) | |
9 | 6, 7, 8 | 3eqtr4g 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 |