| ref-0-id-0 | propositional calculus |
| ref-0-id-1 | propositional theory |
| ref-0-id-2 | axiom one |
| ref-0-id-3 | axiom two |
| ref-0-id-4 | axiom three |
| ref-0-id-5 | mp |
| ref-0-id-6 | mendelson lemma one eight |
| ref-0-id-7 | * imply * |
The pyk compiler, version 0.grue.20050603 by Klaus Grue,