Theorem frege10

Description: Result commuting antecedents within an antecedent. Proposition 10 of Frege1879 p. 36. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

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