Theorem rspc3v 3222

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

Hypotheses

Ref	Expression
rspc3v.1
rspc3v.2
rspc3v.3

Assertion

Ref	Expression
rspc3v

Distinct variable groups:   ,   ,   ,   ,,,   ,,   ,   ,   ,S,   ,,,

Proof of Theorem rspc3v

Step	Hyp	Ref	Expression
1		rspc3v.1	. . . . 5
2	1	ralbidv 2896	. . . 4
3		rspc3v.2	. . . . 5
4	3	ralbidv 2896	. . . 4
5	2, 4	rspc2v 3219	. . 3
6		rspc3v.3	. . . 4
7	6	rspcv 3206	. . 3
8	5, 7	sylan9 657	. 2
9	8	3impa 1191	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  A.wral 2807

This theorem is referenced by:  swopolem  4814  isopolem  6241  caovassg  6473  caovcang  6476  caovordig  6480  caovordg  6482  caovdig  6489  caovdirg  6492  caofass  6574  caoftrn  6575  prslem  15560  posi  15579  latdisdlem  15819  dlatmjdi  15824  sgrpass  15917  gaass  16335  islmodd  17518  lsscl  17589  assalem  17965  psmettri2  20813  xmettri2  20843  axtgcgrid  23860  axtg5seg  23862  axtgpasch  23864  axtgupdim2  23869  axtgeucl  23870  tgdim01  23898  f1otrgitv  24173  grpoass  25205  isgrp2d  25237  rngodi  25387  rngodir  25388  rngoass  25389  vcdi  25445  vcdir  25446  vcass  25447  lnolin  25669  lnopl  26833  lnfnl  26850  omndadd  27696  rngdir  32688  lfli  34786  cvlexch1  35053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111