Theorem rexlimdva2 3246

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 423	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3242	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  r19.29an  3247  r19.29a  3248  otiunsndisj  5375  dffo3  6845  omlimcl  8187  cfflb  9670  cfcof  9685  alephval2  9983  pwcfsdom  9994  recexsr  10518  zdiv  12040  modmuladd  13276  ssnn0fi  13348  2cshwcshw  14178  wrdl3s3  14317  s3iunsndisj  14319  odd2np1  15682  mod2eq1n2dvds  15688  m1expo  15716  dvdsnprmd  16024  ncoprmlnprm  16058  lspsneleq  19880  psgndif  20291  islinds4  20524  cply1coe0bi  20929  mat1dimcrng  21082  smatvscl  21129  cpmatinvcl  21322  pmatcollpw3fi1lem2  21392  fctop  21609  cctop  21611  neindisj  21722  innei  21730  restcld  21777  isnrm3  21964  dis2ndc  22065  fgcl  22483  ufileu  22524  bcthlem5  23932  iundisj  24152  vitalilem2  24213  dcubic  25432  2lgslem1c  25977  2lgslem3a1  25984  2lgslem3b1  25985  2lgslem3c1  25986  2lgslem3d1  25987  f1otrg  26665  umgrnloop  26901  erclwwlkeqlen  27804  erclwwlktr  27807  erclwwlkneqlen  27853  eleclclwwlkn  27861  umgr3v3e3cycl  27969  cusconngr  27976  eucrctshift  28028  2pthfrgr  28069  grpoinvf  28315  nmosetre  28547  blocnilem  28587  shsel3  29098  normcan  29359  nmfnsetre  29660  superpos  30137  iundisjfi  30545  indf1ofs  31395  esumcst  31432  eulerpartlemgh  31746  afsval  32052  fmlasuc  32746  satffunlem2lem2  32766  trpredtr  33182  brsegle2  33683  heicant  35092  itg2gt0cn  35112  sdclem1  35181  sstotbnd3  35214  prtlem10  36161  prjspeclsp  39606  dffltz  39615  diophrw  39700  eldioph2b  39704  diophin  39713  rexrabdioph  39735  jm2.26a  39941  jm2.27  39949  suplesup  41971  uzub  42068  supminfxr  42103  infrpgernmpt  42104  limsuppnflem  42352  limsupubuz  42355  climinf3  42358  limsupre3lem  42374  limsupre3uzlem  42377  limsupvaluz2  42380  supcnvlimsup  42382  limsupresxr  42408  liminfresxr  42409  liminflelimsuplem  42417  limsupgtlem  42419  liminfvalxr  42425  liminfreuzlem  42444  cnrefiisplem  42471  xlimmnfvlem2  42475  xlimpnfvlem2  42479  stoweidlem61  42703  carageniuncllem2  43161  icoresmbl  43182  hspmbllem2  43266  ovnovollem3  43297  smflimlem2  43405  smflimlem4  43407  smfmullem3  43425  smfinflem  43448  smfliminflem  43461  otiunsndisjX  43835  sprsymrelf1lem  44008  fmtnoprmfac2lem1  44083  fmtnofac1  44087  lighneallem2  44124  dfodd6  44155  dfeven4  44156  m1expevenALTV  44165  opoeALTV  44201  opeoALTV  44202  mogoldbb  44303  nnsum4primeseven  44318  uzlidlring  44553  islindeps2  44892  isldepslvec2  44894  m1modmmod  44935  eenglngeehlnmlem1  45151