Theorem rspc3ev

Description: 3-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012)

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

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		simpl1	|- ( ( ( A e. R /\ B e. S /\ C e. T ) /\ ps ) -> A e. R )
5		simpl2	|- ( ( ( A e. R /\ B e. S /\ C e. T ) /\ ps ) -> B e. S )
6	3	rspcev	|- ( ( C e. T /\ ps ) -> E. z e. T th )
7	6	3ad2antl3	|- ( ( ( A e. R /\ B e. S /\ C e. T ) /\ ps ) -> E. z e. T th )
8	1	rexbidv	|- ( x = A -> ( E. z e. T ph <-> E. z e. T ch ) )
9	2	rexbidv	|- ( y = B -> ( E. z e. T ch <-> E. z e. T th ) )
10	8 9	rspc2ev	|- ( ( A e. R /\ B e. S /\ E. z e. T th ) -> E. x e. R E. y e. S E. z e. T ph )
11	4 5 7 10	syl3anc	|- ( ( ( A e. R /\ B e. S /\ C e. T ) /\ ps ) -> E. x e. R E. y e. S E. z e. T ph )