Metamath Proof Explorer

Theorem rp-misc1-frege

Description: Double-use of ax-frege2 . (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	rp-misc1-frege	\|- ( ( ( ph -> ( ps -> ch ) ) -> ( ph -> ps ) ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )

Proof

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

Step

Hyp

Ref

Expression

ax-frege2

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

ax-frege2

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

1 2

ax-mp

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