Theorem bj-alanim

Description: Closed form of alanimi . (Contributed by BJ, 6-May-2019)

	Ref	Expression
Assertion	bj-alanim	|- ( A. x ( ( ph /\ ps ) -> ch ) -> ( ( A. x ph /\ A. x ps ) -> A. x ch ) )

Proof

Step	Hyp	Ref	Expression
1		pm3.3	|- ( ( ( ph /\ ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
2	1	alimi	|- ( A. x ( ( ph /\ ps ) -> ch ) -> A. x ( ph -> ( ps -> ch ) ) )
3		al2im	|- ( A. x ( ph -> ( ps -> ch ) ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) )
4	2 3	syl	|- ( A. x ( ( ph /\ ps ) -> ch ) -> ( A. x ph -> ( A. x ps -> A. x ch ) ) )
5	4	impd	|- ( A. x ( ( ph /\ ps ) -> ch ) -> ( ( A. x ph /\ A. x ps ) -> A. x ch ) )