Metamath Proof Explorer

Table of Contents - 21.40.3.3. Primitive equivalent of ax-groth

  1. expandan
  2. expandexn
  3. expandral
  4. expandrexn
  5. expandrex
  6. expanduniss
  7. ismnuprim
  8. rr-grothprimbi
  9. inagrud
  10. inaex
  11. gruex
  12. rr-groth
  13. rr-grothprim
  14. ismnushort
  15. dfuniv2
  16. rr-grothshortbi
  17. rr-grothshort