Theorem rspc3v 3219

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 2893	. . . 4 |- ( x = A -> ( A. z e. T ph <-> A. z e. T ch ) )
3		rspc3v.2	. . . . 5 |- ( y = B -> ( ch <-> th ) )
4	3	ralbidv 2893	. . . 4 |- ( y = B -> ( A. z e. T ch <-> A. z e. T th ) )
5	2, 4	rspc2v 3216	. . 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 3203	. . 3 |- ( C e. T -> ( A. z e. T th -> ps ) )
8	5, 7	sylan9 655	. 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 1189	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 367   /\ w3a 971   = wceq 1398   e. wcel 1823   A.wral 2804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108

This theorem is referenced by:  swopolem  4798  isopolem  6216  caovassg  6446  caovcang  6449  caovordig  6453  caovordg  6455  caovdig  6462  caovdirg  6465  caofass  6547  caoftrn  6548  prslem  15759  posi  15778  latdisdlem  16018  dlatmjdi  16023  sgrpass  16116  gaass  16534  islmodd  17713  lsscl  17784  assalem  18160  psmettri2  20979  xmettri2  21009  axtgcgrid  24058  axtg5seg  24060  axtgpasch  24062  axtgupdim2  24067  axtgeucl  24068  tgdim01  24099  f1otrgitv  24375  grpoass  25403  isgrp2d  25435  rngodi  25585  rngodir  25586  rngoass  25587  vcdi  25643  vcdir  25644  vcass  25645  lnolin  25867  lnopl  27031  lnfnl  27048  omndadd  27930  rngdir  32942  lfli  35183  cvlexch1  35450