Metamath Proof Explorer

Table of Contents - 17.1.3. Natural deduction examples

These are examples of how natural deduction rules can be applied in Metamath (both as line-for-line translations of ND rules, and as a way to apply deduction forms without being limited to applying ND rules). For more information, see natded and mmnatded.html. Since these examples should not be used within proofs of other theorems, especially in mathboxes, they are marked with "(New usage is discouraged.)".

  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