Metamath Proof Explorer

Theorem frege50

Description: Closed form of jaoi . Proposition 50 of Frege1879 p. 49. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

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

Step

Hyp

Ref

Expression

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

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

1 2

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