Metamath Proof Explorer

Table of Contents - 17.1. Guides (conventions, explanations, and examples)

1. Conventions
   1. conventions
   2. conventions-labels
   3. conventions-comments
2. Natural deduction
   1. natded
3. Natural deduction examples
   1. ex-natded5.2
   2. ex-natded5.2-2
   3. ex-natded5.2i
   4. ex-natded5.3
   5. ex-natded5.3-2
   6. ex-natded5.3i
   7. ex-natded5.5
   8. ex-natded5.7
   9. ex-natded5.7-2
   10. ex-natded5.8
   11. ex-natded5.8-2
   12. ex-natded5.13
   13. ex-natded5.13-2
   14. ex-natded9.20
   15. ex-natded9.20-2
   16. ex-natded9.26
   17. ex-natded9.26-2
4. Definitional examples
   1. ex-or
   2. ex-an
   3. ex-dif
   4. ex-un
   5. ex-in
   6. ex-uni
   7. ex-ss
   8. ex-pss
   9. ex-pw
   10. ex-pr
   11. ex-br
   12. ex-opab
   13. ex-eprel
   14. ex-id
   15. ex-po
   16. ex-xp
   17. ex-cnv
   18. ex-co
   19. ex-dm
   20. ex-rn
   21. ex-res
   22. ex-ima
   23. ex-fv
   24. ex-1st
   25. ex-2nd
   26. 1kp2ke3k
   27. ex-fl
   28. ex-ceil
   29. ex-mod
   30. ex-exp
   31. ex-fac
   32. ex-bc
   33. ex-hash
   34. ex-sqrt
   35. ex-abs
   36. ex-dvds
   37. ex-gcd
   38. ex-lcm
   39. ex-prmo
5. Other examples
   1. aevdemo
   2. ex-ind-dvds
   3. ex-fpar