Metamath Proof Explorer
Table of Contents - 5.7.10. Subwords of concatenations
- swrdccatfn
- swrdccatin1
- pfxccatin12lem4
- pfxccatin12lem2a
- pfxccatin12lem1
- swrdccatin2
- pfxccatin12lem2c
- pfxccatin12lem2
- pfxccatin12lem3
- pfxccatin12
- pfxccat3
- swrdccat
- pfxccatpfx1
- pfxccatpfx2
- pfxccat3a
- swrdccat3blem
- swrdccat3b
- pfxccatid
- ccats1pfxeqbi
- swrdccatin1d
- swrdccatin2d
- pfxccatin12d
- reuccatpfxs1lem
- reuccatpfxs1
- reuccatpfxs1v