Metamath Proof Explorer

Table of Contents - 21.18.5. Short axioms written in primitive symbols

  1. mh-inf3f1
  2. mh-inf3sn
  3. mh-prprimbi
  4. mh-unprimbi
  5. mh-regprimbi
  6. mh-infprim1bi
  7. mh-infprim2bi
  8. mh-infprim3bi