# 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 )`
` |-  ( ( ( 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 )`