Theorem rexlimdva2 3289

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∃wrex 3141

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-ral 3145  df-rex 3146

This theorem is referenced by:  r19.29an  3290  r19.29a  3291  otiunsndisj  5412  dffo3  6870  omlimcl  8206  cfflb  9683  cfcof  9698  alephval2  9996  pwcfsdom  10007  recexsr  10531  zdiv  12055  modmuladd  13284  ssnn0fi  13356  2cshwcshw  14189  wrdl3s3  14328  s3iunsndisj  14330  odd2np1  15692  mod2eq1n2dvds  15698  m1expo  15728  dvdsnprmd  16036  ncoprmlnprm  16070  lspsneleq  19889  cply1coe0bi  20470  psgndif  20748  islinds4  20981  mat1dimcrng  21088  smatvscl  21135  cpmatinvcl  21327  pmatcollpw3fi1lem2  21397  fctop  21614  cctop  21616  neindisj  21727  innei  21735  restcld  21782  isnrm3  21969  dis2ndc  22070  fgcl  22488  ufileu  22529  bcthlem5  23933  iundisj  24151  vitalilem2  24212  dcubic  25426  2lgslem1c  25971  2lgslem3a1  25978  2lgslem3b1  25979  2lgslem3c1  25980  2lgslem3d1  25981  f1otrg  26659  umgrnloop  26895  erclwwlkeqlen  27799  erclwwlktr  27802  erclwwlkneqlen  27849  eleclclwwlkn  27857  umgr3v3e3cycl  27965  cusconngr  27972  eucrctshift  28024  2pthfrgr  28065  grpoinvf  28311  nmosetre  28543  blocnilem  28583  shsel3  29094  normcan  29355  nmfnsetre  29656  superpos  30133  iundisjfi  30521  indf1ofs  31287  esumcst  31324  eulerpartlemgh  31638  afsval  31944  fmlasuc  32635  satffunlem2lem2  32655  trpredtr  33071  brsegle2  33572  heicant  34929  itg2gt0cn  34949  sdclem1  35020  sstotbnd3  35056  prtlem10  36003  prjspeclsp  39269  dffltz  39278  diophrw  39363  eldioph2b  39367  diophin  39376  rexrabdioph  39398  jm2.26a  39604  jm2.27  39612  suplesup  41614  uzub  41712  supminfxr  41747  infrpgernmpt  41748  limsuppnflem  41998  limsupubuz  42001  climinf3  42004  limsupre3lem  42020  limsupre3uzlem  42023  limsupvaluz2  42026  supcnvlimsup  42028  limsupresxr  42054  liminfresxr  42055  liminflelimsuplem  42063  limsupgtlem  42065  liminfvalxr  42071  liminfreuzlem  42090  cnrefiisplem  42117  xlimmnfvlem2  42121  xlimpnfvlem2  42125  stoweidlem61  42353  carageniuncllem2  42811  icoresmbl  42832  hspmbllem2  42916  ovnovollem3  42947  smflimlem2  43055  smflimlem4  43057  smfmullem3  43075  smfinflem  43098  smfliminflem  43111  otiunsndisjX  43485  sprsymrelf1lem  43660  fmtnoprmfac2lem1  43735  fmtnofac1  43739  lighneallem2  43778  dfodd6  43809  dfeven4  43810  m1expevenALTV  43819  opoeALTV  43855  opeoALTV  43856  mogoldbb  43957  nnsum4primeseven  43972  uzlidlring  44207  islindeps2  44545  isldepslvec2  44547  m1modmmod  44588  eenglngeehlnmlem1  44731