Metamath Proof Explorer


Table of Contents - 20.25.3. Rederive new axioms ax-4, ax-10, ax-6, ax-12, ax-13 from old

Theorems ax12fromc15 and ax13fromc9 require some intermediate theorems that are included in this section.

  1. axc5
  2. ax4fromc4
  3. ax10fromc7
  4. ax6fromc10
  5. hba1-o
  6. axc4i-o
  7. equid1
  8. equcomi1
  9. aecom-o
  10. aecoms-o
  11. hbae-o
  12. dral1-o
  13. ax12fromc15
  14. ax13fromc9