Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > minimp | Structured version Visualization version GIF version |
Description: A single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. Among single axioms of this length, it is the one with simplest antecedents (i.e., in the corresponding ordering of binary trees which first compares left subtrees, it is the first one). (Contributed by BJ, 4-Apr-2021.) |
Ref | Expression |
---|---|
minimp | ⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jarr 106 | . . . 4 ⊢ (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → (𝜒 → 𝜏))) | |
2 | 1 | a2d 29 | . . 3 ⊢ (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏))) |
3 | 2 | com12 32 | . 2 ⊢ ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))) |
4 | 3 | a1i 11 | 1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: minimp-syllsimp 1629 minimp-ax2c 1631 |
Copyright terms: Public domain | W3C validator |