Solved it, thank you!
Op vrijdag 11 augustus 2023 om 17:48:51 UTC+2 schreef di@gmail.com:
> Actually you have the same syntax error in a1 and a2, the outermost
> implication should be surrounded in parentheses. Since you declared the
> implication symbol with parentheses around it they are
Actually you have the same syntax error in a1 and a2, the outermost
implication should be surrounded in parentheses. Since you declared the
implication symbol with parentheses around it they are required for any
implication and cannot be omitted.
On Fri, Aug 11, 2023 at 11:47 AM Mario Carneiro
you have a syntax error in `maj` , it should read |- ( p -> q ) instead of
|- p -> q. With the incorrect statement it won't be able to unify when you
try to apply it.
On Fri, Aug 11, 2023 at 11:45 AM Jeroen van Rensen <
jeroenvanren...@gmail.com> wrote:
> Hello everyone,
>
> I'm new to Metamath
Hello everyone,
I'm new to Metamath and it looks really cool!
I'm trying to prove the following statement (in order to prove p -> p):
|- ( ( p -> ( p -> p ) ) -> ( p -> p ) )
And this is my entire database:
```
$c -> ! ( ) wff |- $.
$v p q r $.
wp $f wff p $.
wq $f wff q $.
wr $f wff r $.
