Metamath Proof Explorer

Table of Contents - 20.25.4. Legacy theorems using obsolete axioms

These theorems were mostly intended to study properties of the older axiom schemes and are not useful outside of this section. They should not be used outside of this section. They may be deleted when they are deemed to no longer be of interest.

  1. ax5ALT
  2. sps-o
  3. hbequid
  4. nfequid-o
  5. axc5c7
  6. axc5c7toc5
  7. axc5c7toc7
  8. axc711
  9. nfa1-o
  10. axc711toc7
  11. axc711to11
  12. axc5c711
  13. axc5c711toc5
  14. axc5c711toc7
  15. axc5c711to11
  16. equidqe
  17. axc5sp1
  18. equidq
  19. equid1ALT
  20. axc11nfromc11
  21. naecoms-o
  22. hbnae-o
  23. dvelimf-o
  24. dral2-o
  25. aev-o
  26. ax5eq
  27. dveeq2-o
  28. axc16g-o
  29. dveeq1-o
  30. dveeq1-o16
  31. ax5el
  32. axc11n-16
  33. dveel2ALT
  34. ax12f
  35. ax12eq
  36. ax12el
  37. ax12indn
  38. ax12indi
  39. ax12indalem
  40. ax12inda2ALT
  41. ax12inda2
  42. ax12inda
  43. ax12v2-o
  44. ax12a2-o
  45. axc11-o
  46. fsumshftd
  47. ax-riotaBAD
  48. riotaclbgBAD
  49. riotaclbBAD
  50. riotasvd
  51. riotasv2d
  52. riotasv2s
  53. riotasv
  54. riotasv3d