Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ccats1val2 Structured version   Unicode version

Theorem ccats1val2 12590
 Description: Value of the symbol concatenated with a word. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Proof shortened by Alexander van der Vekens, 14-Oct-2018.)
Assertion
Ref Expression
ccats1val2 Word ++

Proof of Theorem ccats1val2
StepHypRef Expression
1 simp1 995 . . 3 Word Word
2 s1cl 12573 . . . 4 Word
323ad2ant2 1017 . . 3 Word Word
4 lencl 12519 . . . . . . . . 9 Word
54nn0zd 10924 . . . . . . . 8 Word
6 elfzomin 11834 . . . . . . . 8 ..^
75, 6syl 17 . . . . . . 7 Word ..^
8 s1len 12576 . . . . . . . . 9
98oveq2i 6243 . . . . . . . 8
109oveq2i 6243 . . . . . . 7 ..^ ..^
117, 10syl6eleqr 2499 . . . . . 6 Word ..^
1211adantr 463 . . . . 5 Word ..^
13 eleq1 2472 . . . . . 6 ..^ ..^
1413adantl 464 . . . . 5 Word ..^ ..^
1512, 14mpbird 232 . . . 4 Word ..^
16153adant2 1014 . . 3 Word ..^
17 ccatval2 12555 . . 3 Word Word ..^ ++
181, 3, 16, 17syl3anc 1228 . 2 Word ++
19 oveq1 6239 . . . . 5
20193ad2ant3 1018 . . . 4 Word
214nn0cnd 10813 . . . . . 6 Word
2221subidd 9873 . . . . 5 Word
23223ad2ant1 1016 . . . 4 Word
2420, 23eqtrd 2441 . . 3 Word
2524fveq2d 5807 . 2 Word
26 s1fv 12578 . . 3