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

Theorem rspcdva 2720
Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
Hypotheses
Ref Expression
rspcdva.1 (𝑥 = 𝐶 → (𝜓𝜒))
rspcdva.2 (𝜑 → ∀𝑥𝐴 𝜓)
rspcdva.3 (𝜑𝐶𝐴)
Assertion
Ref Expression
rspcdva (𝜑𝜒)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rspcdva
StepHypRef Expression
1 rspcdva.3 . 2 (𝜑𝐶𝐴)
2 rspcdva.2 . 2 (𝜑 → ∀𝑥𝐴 𝜓)
3 rspcdva.1 . . 3 (𝑥 = 𝐶 → (𝜓𝜒))
43rspcv 2711 . 2 (𝐶𝐴 → (∀𝑥𝐴 𝜓𝜒))
51, 2, 4sylc 61 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1287  wcel 1436  wral 2355
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-v 2617
This theorem is referenced by:  frirrg  4151  wetriext  4365  tfisi  4375  omsinds  4408  grprinvlem  5796  grprinvd  5797  suppssov1  5810  caofref  5833  caofinvl  5834  tfrlem1  6027  tfrlem5  6033  tfr1onlemsucfn  6059  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfr1onlemaccex  6067  tfr1onlemres  6068  tfrcllemsucfn  6072  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllembfn  6076  tfrcllemaccex  6080  tfrcllemres  6081  tfrcl  6083  rdgon  6105  frecabcl  6118  undifdcss  6585  enomnilem  6738  fodjuomnilem0  6746  fodjuomnilemres  6747  prltlu  6990  cauappcvgprlemm  7148  caucvgprlemm  7171  caucvgprprlemml  7197  caucvgsrlemgt1  7284  caucvgsr  7291  axcaucvglemcau  7377  axcaucvglemres  7378  exbtwnzlemstep  9587  apbtwnz  9609  frecuzrdgsuc  9749  frecuzrdgg  9751  frecuzrdgsuctlem  9758  uzsinds  9776  iseqovex  9787  iseqvalt  9790  iseq1  9791  iseq1t  9792  iseqfcl  9793  iseqfclt  9794  iseqcl  9795  iseqp1  9796  iseqp1t  9797  iseqoveq  9798  iseqfveq2  9802  iseqfveq  9804  iseqshft2  9806  monoord  9809  monoord2  9810  isermono  9811  iseqsplit  9812  iseqcaopr3  9814  iseqf1olemkle  9817  iseqf1olemklt  9818  iseqf1olemjpcl  9828  iseqf1olemqpcl  9829  iseqf1olemfvp  9830  iseqf1olemqsumkj  9831  iseqf1olemqsum  9833  iseqf1oleml  9836  iseqf1o  9837  iseqid3s  9841  iseqid  9842  iseqid2  9843  iseqhomo  9844  iseqz  9845  zfz1isolemiso  10140  cvg1nlemcau  10312  cvg1nlemres  10313  recvguniq  10323  resqrexlemgt0  10348  resqrexlemoverl  10349  resqrexlemglsq  10350  climi  10568  climcn1  10589  serif0  10631  fisumcvg  10656  isummolem2  10661  isummo  10662  fisum  10665  isumz  10667  fsumf1o  10668  isumss  10669  fisumss  10670  bezoutlemmain  10862  bezoutlemex  10865  bezoutlemzz  10866  bezoutlemmo  10870  bezoutlemle  10872  bezoutlemsup  10873  prmind2  10977  nnsf  11333  nninfalllemn  11336  nninfalllem1  11337  nninfsellemeqinf  11346
  Copyright terms: Public domain W3C validator