Substitute wff for a variable

[Jeroen van Rensen]

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 $.

wim $a wff ( p -> q ) $.
wn $a wff ! p $.

a1 $a |- p -> ( q -> p ) $.
a2 $a |- ( p -> ( q -> r ) ) -> ( ( p -> q ) -> ( p -> r ) ) $.

${
    min $e |- p $.
    maj $e |- p -> q $.
    mp $a |- q $.
$}

lem1 $p |- ( ( p -> ( p -> p ) ) -> ( p -> p ) ) $.

```

For the proof I use a modus ponens, where the minor part is: p -> ((p -> p) -> p), from axiom a1.

The major part I can't get to work. The idea is to use axiom a2, substituting p = p, q = p -> p and r = p.

When I try to assign a2 to the right step, I get this message that I don't understand:

```

MM-PA> assign 6 a2
?Statement "a2" cannot be unified with step 6.

```

What should I do? How can I substitute a wff (p -> p) for a variable (q)?

[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.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/23a2913d-c5a1-4c42-a809-5f6dba8aab77n%40googlegroups.com.

[Mario Carneiro]

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.

[Jeroen van Rensen]

Solved it, thank you!

Op vrijdag 11 augustus 2023 om 17:48:51 UTC+2 schreef di....@gmail.com: