Step |
Hyp |
Ref |
Expression |
1 |
|
cofcutrd.1 |
âĒ ( ð â ðī <<s ðĩ ) |
2 |
|
cofcutrd.2 |
âĒ ( ð â ð = ( ðī |s ðĩ ) ) |
3 |
|
cofcutr |
âĒ ( ( ðī <<s ðĩ â§ ð = ( ðī |s ðĩ ) ) â ( â ðĨ â ( L â ð ) â ðĶ â ðī ðĨ âĪs ðĶ â§ â ð§ â ( R â ð ) â ðĪ â ðĩ ðĪ âĪs ð§ ) ) |
4 |
1 2 3
|
syl2anc |
âĒ ( ð â ( â ðĨ â ( L â ð ) â ðĶ â ðī ðĨ âĪs ðĶ â§ â ð§ â ( R â ð ) â ðĪ â ðĩ ðĪ âĪs ð§ ) ) |
5 |
4
|
simprd |
âĒ ( ð â â ð§ â ( R â ð ) â ðĪ â ðĩ ðĪ âĪs ð§ ) |