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.)".