ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rspcdva Unicode version

Theorem rspcdva 2727
Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
Hypotheses
Ref Expression
rspcdva.1  |-  ( x  =  C  ->  ( ps 
<->  ch ) )
rspcdva.2  |-  ( ph  ->  A. x  e.  A  ps )
rspcdva.3  |-  ( ph  ->  C  e.  A )
Assertion
Ref Expression
rspcdva  |-  ( ph  ->  ch )
Distinct variable groups:    x, A    x, C    ch, x
Allowed substitution hints:    ph( x)    ps( x)

Proof of Theorem rspcdva
StepHypRef Expression
1 rspcdva.3 . 2  |-  ( ph  ->  C  e.  A )
2 rspcdva.2 . 2  |-  ( ph  ->  A. x  e.  A  ps )
3 rspcdva.1 . . 3  |-  ( x  =  C  ->  ( ps 
<->  ch ) )
43rspcv 2718 . 2  |-  ( C  e.  A  ->  ( A. x  e.  A  ps  ->  ch ) )
51, 2, 4sylc 61 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1289    e. wcel 1438   A.wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-v 2621
This theorem is referenced by:  frirrg  4168  wetriext  4382  tfisi  4392  omsinds  4425  grprinvlem  5821  grprinvd  5822  suppssov1  5835  caofref  5858  caofinvl  5859  tfrlem1  6055  tfrlem5  6061  tfr1onlemsucfn  6087  tfr1onlemsucaccv  6088  tfr1onlembxssdm  6090  tfr1onlembfn  6091  tfr1onlemaccex  6095  tfr1onlemres  6096  tfrcllemsucfn  6100  tfrcllemsucaccv  6101  tfrcllembxssdm  6103  tfrcllembfn  6104  tfrcllemaccex  6108  tfrcllemres  6109  tfrcl  6111  rdgon  6133  frecabcl  6146  undifdcss  6613  enomnilem  6773  fodjuomnilem0  6781  fodjuomnilemres  6782  prltlu  7025  cauappcvgprlemm  7183  caucvgprlemm  7206  caucvgprprlemml  7232  caucvgsrlemgt1  7319  caucvgsr  7326  axcaucvglemcau  7412  axcaucvglemres  7413  exbtwnzlemstep  9624  apbtwnz  9646  frecuzrdgsuc  9786  frecuzrdgg  9788  frecuzrdgsuctlem  9795  uzsinds  9813  iseqovex  9835  iseqvalt  9838  seq3val  9839  iseq1  9840  iseq1t  9841  seq3-1  9842  iseqfcl  9843  iseqfclt  9844  seqf  9845  iseqcl  9846  iseqp1  9847  iseqp1t  9848  seq3p1  9849  iseqoveq  9850  seq3clss  9852  iseqfveq2  9855  seq3fveq2  9857  iseqfveq  9859  seq3fveq  9860  seq3feq  9862  iseqshft2  9863  monoord  9869  monoord2  9870  isermono  9871  seq3split  9872  iseqsplit  9873  iseqcaopr3  9875  iseqf1olemkle  9878  iseqf1olemklt  9879  iseqf1olemjpcl  9889  iseqf1olemqpcl  9890  iseqf1olemfvp  9891  seq3f1olemqsumkj  9892  seq3f1olemqsum  9894  seq3f1oleml  9897  seq3f1o  9898  iseqid3s  9903  iseqid  9904  seq3id2  9905  iseqid2  9906  iseqhomo  9907  iseqz  9908  seq3homo  9909  ser3ge0  9917  zfz1isolemiso  10209  seq3shft  10237  cvg1nlemcau  10382  cvg1nlemres  10383  recvguniq  10393  resqrexlemgt0  10418  resqrexlemoverl  10419  resqrexlemglsq  10420  climi  10639  climcn1  10661  serif0  10705  fisumcvg  10730  fsum3cvg  10731  isummolem2  10736  isummo  10737  fisum  10742  fsum3  10743  isumz  10745  fsumf1o  10746  isumss  10747  fisumss  10748  isumss2  10749  fisumcvg2  10750  fisumcvg3  10752  fisumser  10753  fsumsplit  10764  fsumm1  10773  fsum1p  10775  isummulc2  10783  fisumcom2  10795  fsumge1  10818  telfsumo  10823  telfsumo2  10824  fsumparts  10827  isumshft  10846  isum1p  10848  isumnn0nn  10849  isumrpcl  10850  cvgratnnlemnexp  10879  cvgratnnlemmn  10880  cvgratnnlemseq  10881  cvgratnnlemabsle  10882  cvgratnnlemfm  10884  cvgratnnlemrate  10885  cvgratnn  10886  cvgratz  10887  bezoutlemmain  11080  bezoutlemex  11083  bezoutlemzz  11084  bezoutlemmo  11088  bezoutlemle  11090  bezoutlemsup  11091  prmind2  11195  nnsf  11552  nninfalllemn  11555  nninfalllem1  11556  nninfsellemeqinf  11565
  Copyright terms: Public domain W3C validator