Metamath Proof Explorer

Table of Contents - 21.31.9. Exemplar theorems

These theorems were added for illustration or pedagogical purposes without the intention of being used, but some may still be moved to main and used, of course.

1. iddii
2. bicomdALT
3. alan
4. exor
5. rexor
6. ruvALT
7. sn-wcdeq
8. sq45
9. sum9cubes
10. sn-isghm
11. aprilfools2025
12. Standard replacements of ax-10 , ax-11 , ax-12
    1. nfa1w
    2. eu6w
    3. abbibw
    4. absnw
    5. euabsn2w
    6. sn-tz6.12-2