Theorem minimp 1551

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	⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))

Proof of Theorem minimp

Step	Hyp	Ref	Expression
1		jarr 104	. . . 4 ⊢ (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → (𝜒 → 𝜏)))
2	1	a2d 29	. . 3 ⊢ (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏)))
3	2	com12 32	. 2 ⊢ ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))
4	3	a1i 11	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))

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  1552  minimp-ax2c  1554