Theorem rspc3v

Description: 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005)

	Ref	Expression
Hypotheses	rspc3v.1	|- ( x = A -> ( ph <-> ch ) )
	rspc3v.2	|- ( y = B -> ( ch <-> th ) )
	rspc3v.3	|- ( z = C -> ( th <-> ps ) )
Assertion	rspc3v	|- ( ( A e. R /\ B e. S /\ C e. T ) -> ( A. x e. R A. y e. S A. z e. T ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		rspc3v.1	|- ( x = A -> ( ph <-> ch ) )
2		rspc3v.2	|- ( y = B -> ( ch <-> th ) )
3		rspc3v.3	|- ( z = C -> ( th <-> ps ) )
4	1	ralbidv	|- ( x = A -> ( A. z e. T ph <-> A. z e. T ch ) )
5	2	ralbidv	|- ( y = B -> ( A. z e. T ch <-> A. z e. T th ) )
6	4 5	rspc2v	|- ( ( A e. R /\ B e. S ) -> ( A. x e. R A. y e. S A. z e. T ph -> A. z e. T th ) )
7	3	rspcv	|- ( C e. T -> ( A. z e. T th -> ps ) )
8	6 7	sylan9	|- ( ( ( A e. R /\ B e. S ) /\ C e. T ) -> ( A. x e. R A. y e. S A. z e. T ph -> ps ) )
9	8	3impa	|- ( ( A e. R /\ B e. S /\ C e. T ) -> ( A. x e. R A. y e. S A. z e. T ph -> ps ) )