Theorem rspc3v 3206

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 2880	. . . 4 |- ( x = A -> ( A. z e. T ph <-> A. z e. T ch ) )
3		rspc3v.2	. . . . 5 |- ( y = B -> ( ch <-> th ) )
4	3	ralbidv 2880	. . . 4 |- ( y = B -> ( A. z e. T ch <-> A. z e. T th ) )
5	2, 4	rspc2v 3203	. . 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 3190	. . 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 1190	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 972   = wceq 1381   e. wcel 1802   A.wral 2791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-v 3095

This theorem is referenced by:  swopolem  4795  isopolem  6222  caovassg  6454  caovcang  6457  caovordig  6461  caovordg  6463  caovdig  6470  caovdirg  6473  caofass  6555  caoftrn  6556  prslem  15429  posi  15448  latdisdlem  15688  dlatmjdi  15693  sgrpass  15786  gaass  16204  islmodd  17386  lsscl  17457  assalem  17833  psmettri2  20679  xmettri2  20709  axtgcgrid  23725  axtg5seg  23727  axtgpasch  23729  axtgupdim2  23734  axtgeucl  23735  tgdim01  23763  f1otrgitv  24038  grpoass  25070  isgrp2d  25102  rngodi  25252  rngodir  25253  rngoass  25254  vcdi  25310  vcdir  25311  vcass  25312  lnolin  25534  lnopl  26698  lnfnl  26715  omndadd  27562  lfli  34488  cvlexch1  34755