Theorem rexlimdva2 3168

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  r19.29an  3169  r19.29a  3173  otiunsndisj  5493  dffo3  7087  omlimcl  8551  cfflb  10231  cfcof  10246  alephval2  10545  pwcfsdom  10556  recexsr  11080  zdiv  12654  modmuladd  13937  ssnn0fi  14009  2cshwcshw  14850  wrdl3s3  14987  s3iunsndisj  14993  odd2np1  16387  mod2eq1n2dvds  16393  m1expo  16421  dvdsnprmd  16736  ncoprmlnprm  16775  lspsneleq  21205  rngqiprngimfo  21400  pzriprnglem4  21591  psgndif  21709  islinds4  21942  cply1coe0bi  22419  mat1dimcrng  22591  smatvscl  22638  cpmatinvcl  22831  pmatcollpw3fi1lem2  22901  fctop  23118  cctop  23120  neindisj  23231  innei  23239  restcld  23286  isnrm3  23473  dis2ndc  23574  fgcl  23992  ufileu  24033  bcthlem5  25444  iundisj  25664  vitalilem2  25725  dcubic  26965  2lgslem1c  27511  2lgslem3a1  27518  2lgslem3b1  27519  2lgslem3c1  27520  2lgslem3d1  27521  f1otrg  29125  umgrnloop  29363  erclwwlkeqlen  30275  erclwwlktr  30278  erclwwlkneqlen  30324  eleclclwwlkn  30332  umgr3v3e3cycl  30440  cusconngr  30447  eucrctshift  30499  2pthfrgr  30540  grpoinvf  30789  nmosetre  31021  blocnilem  31061  shsel3  31572  normcan  31833  nmfnsetre  32134  superpos  32611  iundisjfi  33049  indf1ofs  33094  dfufd2  33752  constrextdg2lem  34050  constrextdg2  34051  esumcst  34365  eulerpartlemgh  34680  afsval  34973  fmlasuc  35744  satffunlem2lem2  35764  brsegle2  36467  heicant  38161  itg2gt0cn  38181  sdclem1  38249  sstotbnd3  38282  prtlem10  39496  zdivgd  42953  prjspeclsp  43201  dffltz  43223  diophrw  43347  eldioph2b  43351  diophin  43360  rexrabdioph  43378  jm2.26a  43584  jm2.27  43592  oadif1lem  43963  oadif1  43964  naddgeoa  43978  naddwordnexlem4  43985  suplesup  45914  uzub  46004  supminfxr  46037  infrpgernmpt  46038  limsuppnflem  46283  limsupubuz  46286  climinf3  46289  limsupre3lem  46305  limsupre3uzlem  46308  limsupvaluz2  46311  supcnvlimsup  46313  limsupresxr  46339  liminfresxr  46340  limsupgtlem  46350  liminfvalxr  46356  liminfreuzlem  46375  cnrefiisplem  46402  xlimmnfvlem2  46406  xlimpnfvlem2  46410  stoweidlem61  46634  carageniuncllem2  47095  icoresmbl  47116  hspmbllem2  47200  ovnovollem3  47231  smflimlem2  47345  smflimlem4  47347  smfmullem3  47366  smfinflem  47390  smfliminflem  47403  fsupdm  47415  finfdm  47419  otiunsndisjX  47872  m1modmmod  47957  sprsymrelf1lem  48096  fmtnoprmfac2lem1  48174  fmtnofac1  48178  lighneallem2  48214  dfodd6  48258  dfeven4  48259  m1expevenALTV  48268  opoeALTV  48304  opeoALTV  48305  mogoldbb  48406  nnsum4primeseven  48421  grimgrtri  48570  uzlidlring  48856  islindeps2  49115  isldepslvec2  49117  eenglngeehlnmlem1  49369