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

Theorem rspc3v 3219
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 2893 . . . 4  |-  ( x  =  A  ->  ( A. z  e.  T  ph  <->  A. z  e.  T  ch ) )
3 rspc3v.2 . . . . 5  |-  ( y  =  B  ->  ( ch 
<->  th ) )
43ralbidv 2893 . . . 4  |-  ( y  =  B  ->  ( A. z  e.  T  ch 
<-> 
A. z  e.  T  th ) )
52, 4rspc2v 3216 . . 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 3203 . . 3  |-  ( C  e.  T  ->  ( A. z  e.  T  th  ->  ps ) )
85, 7sylan9 655 . 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 1189 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 184    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108
This theorem is referenced by:  swopolem  4798  isopolem  6216  caovassg  6446  caovcang  6449  caovordig  6453  caovordg  6455  caovdig  6462  caovdirg  6465  caofass  6547  caoftrn  6548  prslem  15759  posi  15778  latdisdlem  16018  dlatmjdi  16023  sgrpass  16116  gaass  16534  islmodd  17713  lsscl  17784  assalem  18160  psmettri2  20979  xmettri2  21009  axtgcgrid  24058  axtg5seg  24060  axtgpasch  24062  axtgupdim2  24067  axtgeucl  24068  tgdim01  24099  f1otrgitv  24375  grpoass  25403  isgrp2d  25435  rngodi  25585  rngodir  25586  rngoass  25587  vcdi  25643  vcdir  25644  vcass  25645  lnolin  25867  lnopl  27031  lnfnl  27048  omndadd  27930  rngdir  32942  lfli  35183  cvlexch1  35450
  Copyright terms: Public domain W3C validator