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

Theorem rspc3v 2906
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
StepHypRef Expression
1 rspc3v.1 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
21ralbidv 2576 . . . 4  |-  ( x  =  A  ->  ( A. z  e.  T  ph  <->  A. z  e.  T  ch ) )
3 rspc3v.2 . . . . 5  |-  ( y  =  B  ->  ( ch 
<->  th ) )
43ralbidv 2576 . . . 4  |-  ( y  =  B  ->  ( A. z  e.  T  ch 
<-> 
A. z  e.  T  th ) )
52, 4rspc2v 2903 . . 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 ) )
76rspcv 2893 . . 3  |-  ( C  e.  T  ->  ( A. z  e.  T  th  ->  ps ) )
85, 7sylan9 638 . 2  |-  ( ( ( A  e.  R  /\  B  e.  S
)  /\  C  e.  T )  ->  ( A. x  e.  R  A. y  e.  S  A. z  e.  T  ph 
->  ps ) )
983impa 1146 1  |-  ( ( A  e.  R  /\  B  e.  S  /\  C  e.  T )  ->  ( A. x  e.  R  A. y  e.  S  A. z  e.  T  ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1632    e. wcel 1696   A.wral 2556
This theorem is referenced by:  swopolem  4339  isopolem  5858  caovassg  6034  caovcang  6037  caovordig  6041  caovordg  6043  caovdig  6050  caovdirg  6053  caofass  6127  caoftrn  6128  prslem  14081  posi  14100  latdisdlem  14308  dlatmjdi  14313  mndlem1  14387  gaass  14767  islmodd  15649  lsscl  15716  assalem  16073  xmettri2  17921  grpoass  20886  isgrp2d  20918  rngodi  21068  rngodir  21069  rngoass  21070  vcdi  21124  vcdir  21125  vcass  21126  lnolin  21348  lnopl  22510  lnfnl  22527  smgrpass2  25444  mndoass2  25463  vecax5b  25562  glmrngo  25585  vecax5c  25586  cmpasso  25876  lfli  29873  cvlexch1  30140
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803
  Copyright terms: Public domain W3C validator