Metamath Proof Explorer
Table of Contents - 21.27.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.
- axc5
- ax4fromc4
- ax10fromc7
- ax6fromc10
- hba1-o
- axc4i-o
- equid1
- equcomi1
- aecom-o
- aecoms-o
- hbae-o
- dral1-o
- ax12fromc15
- ax13fromc9