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

Theorem rspcdva 2716
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 2707 . 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 1285    e. wcel 1434   A.wral 2353
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 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-v 2613
This theorem is referenced by:  frirrg  4134  wetriext  4348  tfisi  4357  grprinvlem  5748  grprinvd  5749  suppssov1  5762  caofref  5785  caofinvl  5786  tfrlem1  5979  tfrlem5  5985  tfr1onlemsucfn  6011  tfr1onlemsucaccv  6012  tfr1onlembxssdm  6014  tfr1onlembfn  6015  tfr1onlemaccex  6019  tfr1onlemres  6020  tfrcllemsucfn  6024  tfrcllemsucaccv  6025  tfrcllembxssdm  6027  tfrcllembfn  6028  tfrcllemaccex  6032  tfrcllemres  6033  tfrcl  6035  rdgon  6057  frecabcl  6070  undifdcss  6469  prltlu  6816  cauappcvgprlemm  6974  caucvgprlemm  6997  caucvgprprlemml  7023  caucvgsrlemgt1  7110  caucvgsr  7117  axcaucvglemcau  7203  axcaucvglemres  7204  exbtwnzlemstep  9411  apbtwnz  9433  frecuzrdgsuc  9573  frecuzrdgg  9575  frecuzrdgsuctlem  9582  uzsinds  9595  iseqovex  9606  iseqvalt  9609  iseq1  9610  iseq1t  9611  iseqfcl  9612  iseqfclt  9613  iseqcl  9614  iseqp1  9615  iseqp1t  9616  iseqoveq  9617  iseqfveq2  9621  iseqfveq  9623  iseqshft2  9625  monoord  9628  monoord2  9629  isermono  9630  iseqsplit  9631  iseqcaopr3  9633  iseqid3s  9639  iseqid  9640  iseqid2  9641  iseqhomo  9642  iseqz  9643  cvg1nlemcau  10096  cvg1nlemres  10097  recvguniq  10107  resqrexlemgt0  10132  resqrexlemoverl  10133  resqrexlemglsq  10134  climi  10352  climcn1  10373  serif0  10415  isumrblem  10425  fisumcvg  10426  bezoutlemmain  10619  bezoutlemex  10622  bezoutlemzz  10623  bezoutlemmo  10627  bezoutlemle  10629  bezoutlemsup  10630  prmind2  10734
  Copyright terms: Public domain W3C validator