Theorem rspc3v 2800

Description: 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.)

Hypotheses

Ref	Expression
rspc3v.1	|- ( x = A -> ( ph <-> ch ) )
rspc3v.2	|- ( y = B -> ( ch <-> th ) )
rspc3v.3	|- ( z = C -> ( th <-> ps ) )

Assertion

Ref	Expression
rspc3v	|- ( ( A e. R /\ B e. S /\ C e. T ) -> ( A. x e. R A. y e. S A. z e. T ph -> ps ) )

Distinct variable groups:   ps, z   ch, x   th, y   x, y, z, A   y, B, z   z, C   x, R   x, S, y   x, T, y, z

Allowed substitution hints:   ph( x, y, z)   ps( x, y)   ch( y, z)   th( x, z)   B( x)   C( x, y)   R( y, z)   S( z)

Proof of Theorem rspc3v

Step	Hyp	Ref	Expression
1		rspc3v.1	. . . . 5 |- ( x = A -> ( ph <-> ch ) )
2	1	ralbidv 2435	. . . 4 |- ( x = A -> ( A. z e. T ph <-> A. z e. T ch ) )
3		rspc3v.2	. . . . 5 |- ( y = B -> ( ch <-> th ) )
4	3	ralbidv 2435	. . . 4 |- ( y = B -> ( A. z e. T ch <-> A. z e. T th ) )
5	2, 4	rspc2v 2797	. . 3 |- ( ( A e. R /\ B e. S ) -> ( A. x e. R A. y e. S A. z e. T ph -> A. z e. T th ) )
6		rspc3v.3	. . . 4 |- ( z = C -> ( th <-> ps ) )
7	6	rspcv 2780	. . 3 |- ( C e. T -> ( A. z e. T th -> ps ) )
8	5, 7	sylan9 406	. 2 |- ( ( ( 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 1176	1 |- ( ( A e. R /\ B e. S /\ C e. T ) -> ( A. x e. R A. y e. S A. z e. T ph -> ps ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   /\ w3a 962   = wceq 1331   e. wcel 1480   A.wral 2414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ral 2419  df-v 2683

This theorem is referenced by:  swopolem  4222  isopolem  5716  isosolem  5718  caovassg  5922  caovcang  5925  caovordig  5929  caovordg  5931  caovdig  5938  caovdirg  5941  caoftrn  6000  psmettri2  12486  xmettri2  12519