Theorem rspc3v 3129

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 2809	. . . 4 |- ( x = A -> ( A. z e. T ph <-> A. z e. T ch ) )
3		rspc3v.2	. . . . 5 |- ( y = B -> ( ch <-> th ) )
4	3	ralbidv 2809	. . . 4 |- ( y = B -> ( A. z e. T ch <-> A. z e. T th ) )
5	2, 4	rspc2v 3126	. . 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 3113	. . 3 |- ( C e. T -> ( A. z e. T th -> ps ) )
8	5, 7	sylan9 667	. 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 1205	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 189   /\ wa 375   /\ w3a 986   = wceq 1447   e. wcel 1890   A.wral 2736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2741  df-v 3014

This theorem is referenced by:  swopolem  4741  isopolem  6221  caovassg  6454  caovcang  6457  caovordig  6461  caovordg  6463  caovdig  6470  caovdirg  6473  caofass  6552  caoftrn  6553  prslem  16186  posi  16205  latdisdlem  16445  dlatmjdi  16450  sgrpass  16543  gaass  16961  islmodd  18107  lsscl  18176  assalem  18550  psmettri2  21335  xmettri2  21365  axtgcgrid  24522  axtg5seg  24524  axtgpasch  24526  axtgupdim2  24530  axtgeucl  24531  tgdim01  24562  f1otrgitv  24911  grpoass  25942  isgrp2d  25974  rngodi  26124  rngodir  26125  rngoass  26126  vcdi  26182  vcdir  26183  vcass  26184  lnolin  26406  lnopl  27578  lnfnl  27595  omndadd  28475  axtgupdim2OLD  29490  lfli  32628  cvlexch1  32895  rngdir  40206