Metamath Proof Explorer

Table of Contents - 20.12. Mathbox for Anthony Hart

1. Propositional Calculus
   1. tb-ax1
   2. tb-ax2
   3. tb-ax3
   4. tbsyl
   5. re1ax2lem
   6. re1ax2
   7. naim1
   8. naim2
   9. naim1i
   10. naim2i
   11. naim12i
   12. nabi1i
   13. nabi2i
   14. nabi12i
   15. w3nand
   16. df-3nand
   17. df3nandALT1
   18. df3nandALT2
   19. andnand1
   20. imnand2
2. Predicate Calculus
   1. nalfal
   2. nexntru
   3. nexfal
   4. neufal
   5. neutru
   6. nmotru
   7. mofal
   8. nrmo
3. Miscellaneous single axioms
   1. meran1
   2. meran2
   3. meran3
   4. waj-ax
   5. lukshef-ax2
   6. arg-ax
4. Connective Symmetry
   1. negsym1
   2. imsym1
   3. bisym1
   4. consym1
   5. dissym1
   6. nandsym1
   7. unisym1
   8. exisym1
   9. unqsym1
   10. amosym1
   11. subsym1