Metamath Proof Explorer

Theorem frege25

Description: Closed form for a1dd . Proposition 25 of Frege1879 p. 42. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	frege25	\|- ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )

Step	Hyp	Ref	Expression
1		frege24	\|- ( ( ps -> ch ) -> ( ps -> ( th -> ch ) ) )
2		frege5	\|- ( ( ( ps -> ch ) -> ( ps -> ( th -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) ) )
3	1 2	ax-mp	\|- ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )

Step

Hyp

Ref

Expression

 |-  ( ( ps -> ch ) -> ( ps -> ( th -> ch ) ) )

 |-  ( ( ( ps -> ch ) -> ( ps -> ( th -> ch ) ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) ) )

1 2

 |-  ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( ps -> ( th -> ch ) ) ) )