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

Theorem splval 12832
 Description: Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
splval splice substr ++ ++ substr

Proof of Theorem splval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-splice 12645 . . 3 splice substr ++ ++ substr
21a1i 11 . 2 splice substr ++ ++ substr
3 simprl 762 . . . . 5
4 fveq2 5872 . . . . . . . . 9
54fveq2d 5876 . . . . . . . 8
65adantl 467 . . . . . . 7
7 ot1stg 6812 . . . . . . . 8
87adantl 467 . . . . . . 7
96, 8sylan9eqr 2483 . . . . . 6
109opeq2d 4188 . . . . 5
113, 10oveq12d 6314 . . . 4 substr substr
12 fveq2 5872 . . . . . 6
1312adantl 467 . . . . 5
14 ot3rdg 6814 . . . . . . 7
15143ad2ant3 1028 . . . . . 6
1615adantl 467 . . . . 5
1713, 16sylan9eqr 2483 . . . 4
1811, 17oveq12d 6314 . . 3 substr ++ substr ++
194fveq2d 5876 . . . . . . 7
2019adantl 467 . . . . . 6
21 ot2ndg 6813 . . . . . . 7
2221adantl 467 . . . . . 6
2320, 22sylan9eqr 2483 . . . . 5
243fveq2d 5876 . . . . 5
2523, 24opeq12d 4189 . . . 4
263, 25oveq12d 6314 . . 3 substr substr
2718, 26oveq12d 6314 . 2 substr ++ ++ substr substr ++ ++ substr
28 elex 3087 . . 3