Theorem minimp 1618

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.)

Assertion

Ref	Expression
minimp	⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))

Proof of Theorem minimp

Step	Hyp	Ref	Expression
1		jarr 106	. . . 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-syllsimp  1619  minimp-ax2c  1621