Theorem rexlimdva2 3155

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 2-Jan-2022.)

Hypothesis

Ref	Expression
rexlimdva2.1	⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
rexlimdva2	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva2

Step	Hyp	Ref	Expression
1		rexlimdva2.1	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
2	1	exp31 418	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3151	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069

This theorem is referenced by:  r19.29an  3156  r19.29a  3160  otiunsndisj  5519  dffo3  7102  omlimcl  8580  cfflb  10256  cfcof  10271  alephval2  10569  pwcfsdom  10580  recexsr  11104  zdiv  12636  modmuladd  13882  ssnn0fi  13954  2cshwcshw  14780  wrdl3s3  14917  s3iunsndisj  14919  odd2np1  16288  mod2eq1n2dvds  16294  m1expo  16322  dvdsnprmd  16631  ncoprmlnprm  16668  lspsneleq  20873  rngqiprngimfo  21060  pzriprnglem4  21253  psgndif  21374  islinds4  21609  cply1coe0bi  22044  mat1dimcrng  22199  smatvscl  22246  cpmatinvcl  22439  pmatcollpw3fi1lem2  22509  fctop  22727  cctop  22729  neindisj  22841  innei  22849  restcld  22896  isnrm3  23083  dis2ndc  23184  fgcl  23602  ufileu  23643  bcthlem5  25076  iundisj  25297  vitalilem2  25358  dcubic  26587  2lgslem1c  27132  2lgslem3a1  27139  2lgslem3b1  27140  2lgslem3c1  27141  2lgslem3d1  27142  f1otrg  28389  umgrnloop  28635  erclwwlkeqlen  29539  erclwwlktr  29542  erclwwlkneqlen  29588  eleclclwwlkn  29596  umgr3v3e3cycl  29704  cusconngr  29711  eucrctshift  29763  2pthfrgr  29804  grpoinvf  30052  nmosetre  30284  blocnilem  30324  shsel3  30835  normcan  31096  nmfnsetre  31397  superpos  31874  iundisjfi  32274  indf1ofs  33322  esumcst  33359  eulerpartlemgh  33675  afsval  33981  fmlasuc  34675  satffunlem2lem2  34695  brsegle2  35385  heicant  36826  itg2gt0cn  36846  sdclem1  36914  sstotbnd3  36947  prtlem10  38038  prjspeclsp  41656  dffltz  41678  diophrw  41799  eldioph2b  41803  diophin  41812  rexrabdioph  41834  jm2.26a  42041  jm2.27  42049  oadif1lem  42431  oadif1  42432  naddgeoa  42447  naddwordnexlem4  42454  suplesup  44347  uzub  44439  supminfxr  44472  infrpgernmpt  44473  limsuppnflem  44724  limsupubuz  44727  climinf3  44730  limsupre3lem  44746  limsupre3uzlem  44749  limsupvaluz2  44752  supcnvlimsup  44754  limsupresxr  44780  liminfresxr  44781  liminflelimsuplem  44789  limsupgtlem  44791  liminfvalxr  44797  liminfreuzlem  44816  cnrefiisplem  44843  xlimmnfvlem2  44847  xlimpnfvlem2  44851  stoweidlem61  45075  carageniuncllem2  45536  icoresmbl  45557  hspmbllem2  45641  ovnovollem3  45672  smflimlem2  45786  smflimlem4  45788  smfmullem3  45807  smfinflem  45831  smfliminflem  45844  fsupdm  45856  finfdm  45860  otiunsndisjX  46285  sprsymrelf1lem  46457  fmtnoprmfac2lem1  46532  fmtnofac1  46536  lighneallem2  46572  dfodd6  46603  dfeven4  46604  m1expevenALTV  46613  opoeALTV  46649  opeoALTV  46650  mogoldbb  46751  nnsum4primeseven  46766  uzlidlring  46915  islindeps2  47251  isldepslvec2  47253  m1modmmod  47294  eenglngeehlnmlem1  47510