This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )