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

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