Metamath Proof Explorer


Theorem minimp

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
Assertion minimp
|- ( ph -> ( ( ps -> ch ) -> ( ( ( th -> ps ) -> ( ch -> ta ) ) -> ( ps -> ta ) ) ) )

Proof

Step Hyp Ref Expression
1 jarr
 |-  ( ( ( th -> ps ) -> ( ch -> ta ) ) -> ( ps -> ( ch -> ta ) ) )
2 1 a2d
 |-  ( ( ( th -> ps ) -> ( ch -> ta ) ) -> ( ( ps -> ch ) -> ( ps -> ta ) ) )
3 2 com12
 |-  ( ( ps -> ch ) -> ( ( ( th -> ps ) -> ( ch -> ta ) ) -> ( ps -> ta ) ) )
4 3 a1i
 |-  ( ph -> ( ( ps -> ch ) -> ( ( ( th -> ps ) -> ( ch -> ta ) ) -> ( ps -> ta ) ) ) )