MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspc3v Unicode version

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
StepHypRef Expression
1 rspc3v.1 . . . . 5
21ralbidv 2896 . . . 4
3 rspc3v.2 . . . . 5
43ralbidv 2896 . . . 4
52, 4rspc2v 3219 . . 3
6 rspc3v.3 . . . 4
76rspcv 3206 . . 3
85, 7sylan9 657 . 2
983impa 1191 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator