Theorem minimp 1654

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 107	. . . 4 ⊢ (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → (𝜒 → 𝜏)))
2	1	a2d 30	. . 3 ⊢ (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → ((𝜓 → 𝜒) → (𝜓 → 𝜏)))
3	2	com12 33	. 2 ⊢ ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))
4	3	a1i 11	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  minimp-syllsimp  1655  minimp-ax2c  1657