# Metamath Proof Explorer

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