Theorem rexlimdva2 3141

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 3137	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  r19.29an  3142  r19.29a  3146  otiunsndisj  5476  dffo3  7056  omlimcl  8515  cfflb  10181  cfcof  10196  alephval2  10495  pwcfsdom  10506  recexsr  11030  zdiv  12574  modmuladd  13848  ssnn0fi  13920  2cshwcshw  14760  wrdl3s3  14897  s3iunsndisj  14903  odd2np1  16280  mod2eq1n2dvds  16286  m1expo  16314  dvdsnprmd  16629  ncoprmlnprm  16667  lspsneleq  21082  rngqiprngimfo  21268  pzriprnglem4  21451  psgndif  21569  islinds4  21802  cply1coe0bi  22258  mat1dimcrng  22433  smatvscl  22480  cpmatinvcl  22673  pmatcollpw3fi1lem2  22743  fctop  22960  cctop  22962  neindisj  23073  innei  23081  restcld  23128  isnrm3  23315  dis2ndc  23416  fgcl  23834  ufileu  23875  bcthlem5  25296  iundisj  25517  vitalilem2  25578  dcubic  26824  2lgslem1c  27372  2lgslem3a1  27379  2lgslem3b1  27380  2lgslem3c1  27381  2lgslem3d1  27382  f1otrg  28955  umgrnloop  29193  erclwwlkeqlen  30106  erclwwlktr  30109  erclwwlkneqlen  30155  eleclclwwlkn  30163  umgr3v3e3cycl  30271  cusconngr  30278  eucrctshift  30330  2pthfrgr  30371  grpoinvf  30619  nmosetre  30851  blocnilem  30891  shsel3  31402  normcan  31663  nmfnsetre  31964  superpos  32441  iundisjfi  32886  indf1ofs  32958  dfufd2  33642  constrextdg2lem  33925  constrextdg2  33926  esumcst  34240  eulerpartlemgh  34555  afsval  34848  fmlasuc  35599  satffunlem2lem2  35619  brsegle2  36322  heicant  37900  itg2gt0cn  37920  sdclem1  37988  sstotbnd3  38021  prtlem10  39235  zdivgd  42701  prjspeclsp  42964  dffltz  42986  diophrw  43110  eldioph2b  43114  diophin  43123  rexrabdioph  43145  jm2.26a  43351  jm2.27  43359  oadif1lem  43730  oadif1  43731  naddgeoa  43745  naddwordnexlem4  43752  suplesup  45692  uzub  45783  supminfxr  45816  infrpgernmpt  45817  limsuppnflem  46062  limsupubuz  46065  climinf3  46068  limsupre3lem  46084  limsupre3uzlem  46087  limsupvaluz2  46090  supcnvlimsup  46092  limsupresxr  46118  liminfresxr  46119  limsupgtlem  46129  liminfvalxr  46135  liminfreuzlem  46154  cnrefiisplem  46181  xlimmnfvlem2  46185  xlimpnfvlem2  46189  stoweidlem61  46413  carageniuncllem2  46874  icoresmbl  46895  hspmbllem2  46979  ovnovollem3  47010  smflimlem2  47124  smflimlem4  47126  smfmullem3  47145  smfinflem  47169  smfliminflem  47182  fsupdm  47194  finfdm  47198  otiunsndisjX  47633  m1modmmod  47712  sprsymrelf1lem  47845  fmtnoprmfac2lem1  47920  fmtnofac1  47924  lighneallem2  47960  dfodd6  47991  dfeven4  47992  m1expevenALTV  48001  opoeALTV  48037  opeoALTV  48038  mogoldbb  48139  nnsum4primeseven  48154  grimgrtri  48303  uzlidlring  48589  islindeps2  48837  isldepslvec2  48839  eenglngeehlnmlem1  49091