Theorem rspec2

Description: Specialization rule for restricted quantification, with two quantifiers. (Contributed by NM, 20-Nov-1994)

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

Proof

Step	Hyp	Ref	Expression
1		rspec2.1	|- A. x e. A A. y e. B ph
2	1	rspec	|- ( x e. A -> A. y e. B ph )
3	2	r19.21bi	|- ( ( x e. A /\ y e. B ) -> ph )