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

Theorem rexlimdva 2526
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
Hypothesis
Ref Expression
rexlimdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rexlimdva (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva
StepHypRef Expression
1 rexlimdva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 114 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 2525 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1465  wrex 2394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-i5r 1500
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-ral 2398  df-rex 2399
This theorem is referenced by:  rexlimdvaa  2527  rexlimivv  2532  rexlimdvv  2533  ralxfrd  4353  rexxfrd  4354  fvelimab  5445  foco2  5623  elunirn  5635  f1elima  5642  tfrlem5  6179  tfrlemibacc  6191  tfrlemibfn  6193  tfr1onlembacc  6207  tfr1onlembfn  6209  tfrcllembacc  6220  tfrcllembfn  6222  frecabcl  6264  nnaordex  6391  nnawordex  6392  ectocld  6463  phpm  6727  dif1enen  6742  fin0  6747  fin0or  6748  fimax2gtri  6763  fidcenum  6812  suplub2ti  6856  supisoex  6864  enomnilem  6978  finomni  6980  exmidfodomrlemeldju  7023  exmidfodomrlemreseldju  7024  ltexnqq  7184  ltbtwnnqq  7191  prarloclem4  7274  prarloc2  7280  genprndl  7297  genprndu  7298  prmuloc2  7343  1idprl  7366  1idpru  7367  cauappcvgprlemdisj  7427  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  caucvgprlemladdrl  7454  recexgt0sr  7549  map2psrprg  7581  suplocsrlem  7584  nntopi  7670  cnegexlem1  7905  cnegexlem2  7906  renegcl  7991  supinfneg  9358  infsupneg  9359  qmulz  9383  icc0r  9677  exbtwnzlemstep  9993  rebtwn2zlemstep  9998  ioo0  10005  ico0  10007  ioc0  10008  modqmuladd  10107  addmodlteq  10139  frec2uzrand  10146  frecuzrdgtcl  10153  frecuzrdgfunlem  10160  hashunlem  10518  shftlem  10556  caucvgre  10721  resqrexlemgt0  10760  rexico  10961  negfi  10967  climuni  11030  climshftlemg  11039  climcn1  11045  serf0  11089  summodclem2  11119  zsumdc  11121  fsum2dlemstep  11171  mertenslem2  11273  dvds1lem  11431  odd2np1lem  11496  odd2np1  11497  sqoddm1div8z  11510  ltoddhalfle  11517  halfleoddlt  11518  m1expo  11524  divalglemeunn  11545  divalglemex  11546  divalglemeuneg  11547  flodddiv4  11558  bezoutlemaz  11618  bezoutlembz  11619  dvdssqim  11639  ncoprmgcdne1b  11697  coprmdvds2  11701  divgcdcoprm0  11709  cncongr1  11711  cncongr2  11712  dvdsnprmd  11733  rpexp  11758  tgcl  12160  innei  12259  cnptoprest  12335  lmss  12342  lmtopcnp  12346  txlm  12375  blssps  12523  blss  12524  blssexps  12525  blssex  12526  mopni3  12580  metrest  12602  metcnp3  12607  mulc1cncf  12672  cncfco  12674  subctctexmid  13123
  Copyright terms: Public domain W3C validator