minimp-syllsimp

Description: Derivation of Syll-Simp ( jarr ) from ax-mp and minimp . (Contributed by BJ, 4-Apr-2021) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	minimp-syllsimp	$⊢ ((φ \to ψ) \to χ) \to (ψ \to χ)$

Proof

Step	Hyp	Ref	Expression
1		minimp	$⊢ (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))$
2		minimp	$⊢ (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))))) \to ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))))))$
3		minimp	$⊢ ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))))) \to ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))))))) \to (((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((φ \to ψ) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))))$
4	2 3	ax-mp	$⊢ ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to (((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((φ \to ψ) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)))$
5		minimp	$⊢ ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to (((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)))) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)))))$
6		minimp	$⊢ ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))$
7		minimp	$⊢ (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to (((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)))) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)))))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to (((((φ \to ψ) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ))))$
8	5 6 7	mp2	$⊢ ((((φ \to ψ) \to (((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to ((((φ \to ψ) \to (φ \to ψ)) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ))) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ))$
9	1 4 8	mp2b	$⊢ ((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)$
10		minimp	$⊢ (φ \to ψ) \to (((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))$
11		minimp	$⊢ ((φ \to ψ) \to (((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ))))) \to (((φ \to ψ) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ))) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to χ) \to χ))) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ))))$
12		minimp	$⊢ (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ))) \to ((((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)))))$
13		minimp	$⊢ (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to χ) \to χ)))$
14		minimp	$⊢ ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ))) \to ((((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)))))) \to (((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to ((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to χ) \to χ)))) \to ((((φ \to ψ) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ))) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to χ) \to χ))) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)))))$
15	12 13 14	mp2	$⊢ (((φ \to ψ) \to (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ))) \to (((((φ \to ψ) \to χ) \to (φ \to ψ)) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to χ) \to χ))) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)))) \to ((((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)))$
16	10 11 15	mp2b	$⊢ (((((φ \to ψ) \to (φ \to ψ)) \to ((((φ \to ψ) \to (φ \to ψ)) \to ((φ \to ψ) \to (φ \to ψ))) \to ((φ \to ψ) \to (φ \to ψ)))) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ))$
17		minimp	$⊢ ((φ \to ψ) \to χ) \to ((((φ \to ψ) \to χ) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to χ) \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to χ) \to ((φ \to ψ) \to χ))) \to (((φ \to ψ) \to χ) \to ((φ \to ψ) \to χ))))$
18		minimp	$⊢ (((φ \to ψ) \to χ) \to ((((φ \to ψ) \to χ) \to ((φ \to ψ) \to χ)) \to (((((φ \to ψ) \to χ) \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to χ) \to ((φ \to ψ) \to χ))) \to (((φ \to ψ) \to χ) \to ((φ \to ψ) \to χ))))) \to ((((φ \to ψ) \to χ) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ))) \to (((ψ \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to (ψ \to χ))) \to (((φ \to ψ) \to χ) \to (ψ \to χ))))$
19		minimp	$⊢ ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ))) \to (((((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ))) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)))) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)))))$
20		minimp	$⊢ ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((ψ \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to (ψ \to χ)))$
21		minimp	$⊢ (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ))) \to (((((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ))) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)))) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)))))) \to ((((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to ((ψ \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to (ψ \to χ)))) \to (((((φ \to ψ) \to χ) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ))) \to (((ψ \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to (ψ \to χ))) \to (((φ \to ψ) \to χ) \to (ψ \to χ)))) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to (((φ \to ψ) \to χ) \to (ψ \to χ)))))$
22	19 20 21	mp2	$⊢ ((((φ \to ψ) \to χ) \to ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ))) \to (((ψ \to ((φ \to ψ) \to χ)) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to (ψ \to χ))) \to (((φ \to ψ) \to χ) \to (ψ \to χ)))) \to (((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to (((φ \to ψ) \to χ) \to (ψ \to χ)))$
23	17 18 22	mp2b	$⊢ ((φ \to ψ) \to (((φ \to ψ) \to χ) \to χ)) \to (((φ \to ψ) \to χ) \to (ψ \to χ))$
24	9 16 23	mp2b	$⊢ ((φ \to ψ) \to χ) \to (ψ \to χ)$

Metamath Proof Explorer

Theorem minimp-syllsimp

Proof