| 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 | axiom four |
| ref-0-id-6 | axiom five |
| ref-0-id-7 | axiom mp |
| ref-0-id-8 | axiom gen |
| ref-0-id-9 | mendelson lemma one eight |
| ref-0-id-10 | mendelson corollary one ten a |
| ref-0-id-11 | mendelson corollary one ten b |
| ref-0-id-12 | mendelson lemma one eleven a |
| ref-0-id-14 | * imply * |
The pyk compiler, version 0.grue.20050502+ by Klaus Grue,