Theorem minimp 1560

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. (Contributed by BJ, 4-Apr-2021.)

Assertion

Ref	Expression
minimp	|- ( ph -> ( ( ps -> ch ) -> ( ( ( th -> ps ) -> ( ch -> ta ) ) -> ( ps -> ta ) ) ) )

Proof of Theorem minimp

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

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-sylsimp  1561  minimp-ax2c  1563