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)?
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/23a2913d-c5a1-4c42-a809-5f6dba8aab77n%40googlegroups.com.
