Metamath Proof Explorer

Theorem al3im

Description: Version of ax-4 for a nested implication. (Contributed by RP, 13-Apr-2020)

		Ref	Expression
	Assertion	al3im	\|- ( A. x ( ph -> ( ps -> ( ch -> th ) ) ) -> ( A. x ph -> ( A. x ps -> ( A. x ch -> A. x th ) ) ) )

Step	Hyp	Ref	Expression
1		alim	\|- ( A. x ( ph -> ( ps -> ( ch -> th ) ) ) -> ( A. x ph -> A. x ( ps -> ( ch -> th ) ) ) )
2		al2im	\|- ( A. x ( ps -> ( ch -> th ) ) -> ( A. x ps -> ( A. x ch -> A. x th ) ) )
3	1 2	syl6	\|- ( A. x ( ph -> ( ps -> ( ch -> th ) ) ) -> ( A. x ph -> ( A. x ps -> ( A. x ch -> A. x th ) ) ) )

Step

Hyp

Ref

Expression

 |-  ( A. x ( ph -> ( ps -> ( ch -> th ) ) ) -> ( A. x ph -> A. x ( ps -> ( ch -> th ) ) ) )

 |-  ( A. x ( ps -> ( ch -> th ) ) -> ( A. x ps -> ( A. x ch -> A. x th ) ) )

1 2

 |-  ( A. x ( ph -> ( ps -> ( ch -> th ) ) ) -> ( A. x ph -> ( A. x ps -> ( A. x ch -> A. x th ) ) ) )