Metamath Proof Explorer

Table of Contents - 21.20.1.1. Derived rules of inference

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

1. bj-mp2c
2. bj-mp2d