Theorem 19.41rg

Description: Closed form of right-to-left implication of 19.41 , Theorem 19.41 of Margaris p. 90. Derived from 19.41rgVD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	19.41rg	|- ( A. x ( ps -> A. x ps ) -> ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) )

Proof

Step	Hyp	Ref	Expression
1		sp	|- ( A. x ( ps -> A. x ps ) -> ( ps -> A. x ps ) )
2		pm3.21	|- ( ps -> ( ph -> ( ph /\ ps ) ) )
3	2	a1i	|- ( ( ps -> A. x ps ) -> ( ps -> ( ph -> ( ph /\ ps ) ) ) )
4	3	al2imi	|- ( A. x ( ps -> A. x ps ) -> ( A. x ps -> A. x ( ph -> ( ph /\ ps ) ) ) )
5		exim	|- ( A. x ( ph -> ( ph /\ ps ) ) -> ( E. x ph -> E. x ( ph /\ ps ) ) )
6	4 5	syl6	|- ( A. x ( ps -> A. x ps ) -> ( A. x ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) )
7	1 6	syld	|- ( A. x ( ps -> A. x ps ) -> ( ps -> ( E. x ph -> E. x ( ph /\ ps ) ) ) )
8	7	com23	|- ( A. x ( ps -> A. x ps ) -> ( E. x ph -> ( ps -> E. x ( ph /\ ps ) ) ) )
9	8	impd	|- ( A. x ( ps -> A. x ps ) -> ( ( E. x ph /\ ps ) -> E. x ( ph /\ ps ) ) )