Metamath Proof Explorer

Theorem frege19

Description: A closed form of syl6 . Proposition 19 of Frege1879 p. 39. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

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

Step

Hyp

Ref

Expression

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

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

1 2

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