Theorem rexlimdva 2624

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

Step	Hyp	Ref	Expression
1		rexlimdva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 2623	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177  ∃wrex 2486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2490  df-rex 2491

This theorem is referenced by:  rexlimdvaa  2625  rexlimivv  2630  rexlimdvv  2631  ralxfrd  4514  rexxfrd  4515  fvelimab  5645  foco2  5832  elunirn  5845  f1elima  5852  mpoexw  6309  tfrlem5  6410  tfrlemibacc  6422  tfrlemibfn  6424  tfr1onlembacc  6438  tfr1onlembfn  6440  tfrcllembacc  6451  tfrcllembfn  6453  frecabcl  6495  nnaordex  6624  nnawordex  6625  ectocld  6698  phpm  6974  dif1enen  6989  fin0  6994  fin0or  6995  fimax2gtri  7010  fidcenum  7070  suplub2ti  7115  supisoex  7123  enomnilem  7252  finomni  7254  enmkvlem  7275  exmidfodomrlemeldju  7320  exmidfodomrlemreseldju  7321  ltexnqq  7534  ltbtwnnqq  7541  prarloclem4  7624  prarloc2  7630  genprndl  7647  genprndu  7648  prmuloc2  7693  1idprl  7716  1idpru  7717  cauappcvgprlemdisj  7777  cauappcvgprlemladdru  7782  cauappcvgprlemladdrl  7783  caucvgprlemladdrl  7804  recexgt0sr  7899  map2psrprg  7931  suplocsrlem  7934  nntopi  8020  cnegexlem1  8260  cnegexlem2  8261  renegcl  8346  aptap  8736  supinfneg  9729  infsupneg  9730  qmulz  9757  elpq  9783  icc0r  10061  exbtwnzlemstep  10403  rebtwn2zlemstep  10408  ioo0  10415  ico0  10417  ioc0  10418  modqmuladd  10524  addmodlteq  10556  frec2uzrand  10563  frecuzrdgtcl  10570  frecuzrdgfunlem  10577  hashunlem  10962  shftlem  11177  caucvgre  11342  resqrexlemgt0  11381  rexico  11582  negfi  11589  climuni  11654  climshftlemg  11663  climcn1  11669  serf0  11713  summodclem2  11743  zsumdc  11745  fsum2dlemstep  11795  mertenslem2  11897  ntrivcvgap  11909  zproddc  11940  fprod2dlemstep  11983  dvds1lem  12163  odd2np1lem  12233  odd2np1  12234  sqoddm1div8z  12247  ltoddhalfle  12254  halfleoddlt  12255  m1expo  12261  divalglemeunn  12282  divalglemex  12283  divalglemeuneg  12284  flodddiv4  12297  bezoutlemaz  12374  bezoutlembz  12375  dvdssqim  12395  ncoprmgcdne1b  12461  coprmdvds2  12465  divgcdcoprm0  12473  cncongr1  12475  cncongr2  12476  dvdsnprmd  12497  rpexp  12525  pythagtriplem1  12638  pc2dvds  12703  difsqpwdvds  12711  oddprmdvds  12727  prmpwdvds  12728  4sqlem11  12774  imasmnd2  13334  dfgrp3mlem  13480  imasgrp2  13496  issubg4m  13579  imasabl  13722  ringinvnzdiv  13862  imasring  13876  dvdsrcl2  13911  dvdsrmul1  13914  isnzr2  13996  lss1d  14195  lssats2  14226  lspsn  14228  dvdsrzring  14415  znunit  14471  znrrg  14472  tgcl  14586  innei  14685  cnptoprest  14761  lmss  14768  lmtopcnp  14772  txlm  14801  blssps  14949  blss  14950  blssexps  14951  blssex  14952  mopni3  15006  metrest  15028  metcnp3  15033  mulc1cncf  15111  cncfco  15113  elply2  15257  gausslemma2dlem1a  15585  lgsquadlem1  15604  2lgsoddprmlem2  15633  subctctexmid  16052