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	$⊢ φ \to ((ψ \to χ) \to (((θ \to ψ) \to (χ \to τ)) \to (ψ \to τ)))$

Proof

Step	Hyp	Ref	Expression
1		jarr	$⊢ ((θ \to ψ) \to (χ \to τ)) \to (ψ \to (χ \to τ))$
2	1	a2d	$⊢ ((θ \to ψ) \to (χ \to τ)) \to ((ψ \to χ) \to (ψ \to τ))$
3	2	com12	$⊢ (ψ \to χ) \to (((θ \to ψ) \to (χ \to τ)) \to (ψ \to τ))$
4	3	a1i	$⊢ φ \to ((ψ \to χ) \to (((θ \to ψ) \to (χ \to τ)) \to (ψ \to τ)))$