Theorem rspec3

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

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

Proof

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