Metamath Proof Explorer

Table of Contents - 21.18.1.1. Derived rules of inference

In this section, we prove a few rules of inference derived from modus ponens ax-mp, and which do not depend on any other axioms.

1. bj-mp2c
2. bj-mp2d