Theorem rspc3v 3221

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 2898	. . . 4 |- ( x = A -> ( A. z e. T ph <-> A. z e. T ch ) )
3		rspc3v.2	. . . . 5 |- ( y = B -> ( ch <-> th ) )
4	3	ralbidv 2898	. . . 4 |- ( y = B -> ( A. z e. T ch <-> A. z e. T th ) )
5	2, 4	rspc2v 3218	. . 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 3205	. . 3 |- ( C e. T -> ( A. z e. T th -> ps ) )
8	5, 7	sylan9 657	. 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 1186	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   <-> wb 184   /\ wa 369   /\ w3a 968   = wceq 1374   e. wcel 1762   A.wral 2809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ral 2814  df-v 3110

This theorem is referenced by:  swopolem  4804  isopolem  6222  caovassg  6450  caovcang  6453  caovordig  6457  caovordg  6459  caovdig  6466  caovdirg  6469  caofass  6551  caoftrn  6552  prslem  15409  posi  15428  latdisdlem  15667  dlatmjdi  15672  mndlem1  15727  gaass  16125  islmodd  17296  lsscl  17367  assalem  17731  psmettri2  20543  xmettri2  20573  axtgcgrid  23583  axtg5seg  23585  axtgpasch  23587  axtgupdim2  23592  axtgeucl  23593  tgdim01  23621  f1otrgitv  23844  grpoass  24869  isgrp2d  24901  rngodi  25051  rngodir  25052  rngoass  25053  vcdi  25109  vcdir  25110  vcass  25111  lnolin  25333  lnopl  26497  lnfnl  26514  omndadd  27346  lfli  33735  cvlexch1  34002