Metamath Proof Explorer

Theorem frege29

Description: Closed form of con3d . Proposition 29 of Frege1879 p. 43. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	frege29	\|- ( ( ph -> ( ps -> ch ) ) -> ( ph -> ( -. ch -> -. ps ) ) )

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

Step

Hyp

Ref

Expression

 |-  ( ( ps -> ch ) -> ( -. ch -> -. ps ) )

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

1 2

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