Metamath Proof Explorer

Theorem frege49

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

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

Proof

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

Step

Hyp

Ref

Expression

frege47

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

frege12

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

1 2

ax-mp

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