Metamath Proof Explorer

Table of Contents - 21.20.1.3. Minimal implicational calculus

Minimal implicational calculus, or intuitionistic implicational calculus, is the logical calculus with axioms ax-mp, ax-1, ax-2.

1. bj-poni
2. bj-nnclav
3. bj-nnclavi
4. bj-nnclavc
5. bj-nnclavci
6. bj-jarrii
7. bj-imim21
8. bj-imim21i
9. bj-imim11
10. bj-imim11i
11. bj-peircestab
12. bj-stabpeirce