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

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
StepHypRef Expression
1 rspc3v.1 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ch ) )
21ralbidv 2809 . . . 4  |-  ( x  =  A  ->  ( A. z  e.  T  ph  <->  A. z  e.  T  ch ) )
3 rspc3v.2 . . . . 5  |-  ( y  =  B  ->  ( ch 
<->  th ) )
43ralbidv 2809 . . . 4  |-  ( y  =  B  ->  ( A. z  e.  T  ch 
<-> 
A. z  e.  T  th ) )
52, 4rspc2v 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 ) )
76rspcv 3113 . . 3  |-  ( C  e.  T  ->  ( A. z  e.  T  th  ->  ps ) )
85, 7sylan9 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 ) )
983impa 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 ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator