Theorem rsp2

Description: Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997)

	Ref	Expression
Assertion	rsp2	|- ( A. x e. A A. y e. B ph -> ( ( x e. A /\ y e. B ) -> ph ) )

Proof

Step	Hyp	Ref	Expression
1		rsp	|- ( A. x e. A A. y e. B ph -> ( x e. A -> A. y e. B ph ) )
2		rsp	|- ( A. y e. B ph -> ( y e. B -> ph ) )
3	1 2	syl6	|- ( A. x e. A A. y e. B ph -> ( x e. A -> ( y e. B -> ph ) ) )
4	3	impd	|- ( A. x e. A A. y e. B ph -> ( ( x e. A /\ y e. B ) -> ph ) )