Theorem rexlimdva2 3215

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  r19.29an  3216  r19.29a  3217  otiunsndisj  5428  dffo3  6960  omlimcl  8371  trpredtr  9408  cfflb  9946  cfcof  9961  alephval2  10259  pwcfsdom  10270  recexsr  10794  zdiv  12320  modmuladd  13561  ssnn0fi  13633  2cshwcshw  14466  wrdl3s3  14605  s3iunsndisj  14607  odd2np1  15978  mod2eq1n2dvds  15984  m1expo  16012  dvdsnprmd  16323  ncoprmlnprm  16360  lspsneleq  20292  psgndif  20719  islinds4  20952  cply1coe0bi  21381  mat1dimcrng  21534  smatvscl  21581  cpmatinvcl  21774  pmatcollpw3fi1lem2  21844  fctop  22062  cctop  22064  neindisj  22176  innei  22184  restcld  22231  isnrm3  22418  dis2ndc  22519  fgcl  22937  ufileu  22978  bcthlem5  24397  iundisj  24617  vitalilem2  24678  dcubic  25901  2lgslem1c  26446  2lgslem3a1  26453  2lgslem3b1  26454  2lgslem3c1  26455  2lgslem3d1  26456  f1otrg  27136  umgrnloop  27381  erclwwlkeqlen  28284  erclwwlktr  28287  erclwwlkneqlen  28333  eleclclwwlkn  28341  umgr3v3e3cycl  28449  cusconngr  28456  eucrctshift  28508  2pthfrgr  28549  grpoinvf  28795  nmosetre  29027  blocnilem  29067  shsel3  29578  normcan  29839  nmfnsetre  30140  superpos  30617  iundisjfi  31019  indf1ofs  31894  esumcst  31931  eulerpartlemgh  32245  afsval  32551  fmlasuc  33248  satffunlem2lem2  33268  brsegle2  34338  heicant  35739  itg2gt0cn  35759  sdclem1  35828  sstotbnd3  35861  prtlem10  36806  prjspeclsp  40372  dffltz  40387  diophrw  40497  eldioph2b  40501  diophin  40510  rexrabdioph  40532  jm2.26a  40738  jm2.27  40746  suplesup  42768  uzub  42861  supminfxr  42894  infrpgernmpt  42895  limsuppnflem  43141  limsupubuz  43144  climinf3  43147  limsupre3lem  43163  limsupre3uzlem  43166  limsupvaluz2  43169  supcnvlimsup  43171  limsupresxr  43197  liminfresxr  43198  liminflelimsuplem  43206  limsupgtlem  43208  liminfvalxr  43214  liminfreuzlem  43233  cnrefiisplem  43260  xlimmnfvlem2  43264  xlimpnfvlem2  43268  stoweidlem61  43492  carageniuncllem2  43950  icoresmbl  43971  hspmbllem2  44055  ovnovollem3  44086  smflimlem2  44194  smflimlem4  44196  smfmullem3  44214  smfinflem  44237  smfliminflem  44250  otiunsndisjX  44658  sprsymrelf1lem  44831  fmtnoprmfac2lem1  44906  fmtnofac1  44910  lighneallem2  44946  dfodd6  44977  dfeven4  44978  m1expevenALTV  44987  opoeALTV  45023  opeoALTV  45024  mogoldbb  45125  nnsum4primeseven  45140  uzlidlring  45375  islindeps2  45712  isldepslvec2  45714  m1modmmod  45755  eenglngeehlnmlem1  45971