| ref-1-id-488 | not * |
| ref-0-id-0 | propcalc |
| ref-0-id-2 | axiom one |
| ref-0-id-3 | axiom two |
| ref-0-id-4 | axiom three |
| ref-0-id-7 | rule mp |
| ref-0-id-9 | mendelson lemma one eight |
| ref-0-id-14 | lemma id |
| ref-0-id-15 | * implies * |
The pyk compiler, version 0.grue.20050603 by Klaus Grue,