Theorem rexlimdva2 3143

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3061

This theorem is referenced by:  r19.29an  3144  r19.29a  3148  otiunsndisj  5495  dffo3  7092  omlimcl  8590  cfflb  10273  cfcof  10288  alephval2  10586  pwcfsdom  10597  recexsr  11121  zdiv  12663  modmuladd  13931  ssnn0fi  14003  2cshwcshw  14844  wrdl3s3  14981  s3iunsndisj  14987  odd2np1  16360  mod2eq1n2dvds  16366  m1expo  16394  dvdsnprmd  16709  ncoprmlnprm  16747  lspsneleq  21076  rngqiprngimfo  21262  pzriprnglem4  21445  psgndif  21562  islinds4  21795  cply1coe0bi  22240  mat1dimcrng  22415  smatvscl  22462  cpmatinvcl  22655  pmatcollpw3fi1lem2  22725  fctop  22942  cctop  22944  neindisj  23055  innei  23063  restcld  23110  isnrm3  23297  dis2ndc  23398  fgcl  23816  ufileu  23857  bcthlem5  25280  iundisj  25501  vitalilem2  25562  dcubic  26808  2lgslem1c  27356  2lgslem3a1  27363  2lgslem3b1  27364  2lgslem3c1  27365  2lgslem3d1  27366  f1otrg  28850  umgrnloop  29087  erclwwlkeqlen  30000  erclwwlktr  30003  erclwwlkneqlen  30049  eleclclwwlkn  30057  umgr3v3e3cycl  30165  cusconngr  30172  eucrctshift  30224  2pthfrgr  30265  grpoinvf  30513  nmosetre  30745  blocnilem  30785  shsel3  31296  normcan  31557  nmfnsetre  31858  superpos  32335  iundisjfi  32773  indf1ofs  32843  dfufd2  33565  constrextdg2lem  33782  constrextdg2  33783  esumcst  34094  eulerpartlemgh  34410  afsval  34703  fmlasuc  35408  satffunlem2lem2  35428  brsegle2  36127  heicant  37679  itg2gt0cn  37699  sdclem1  37767  sstotbnd3  37800  prtlem10  38883  zdivgd  42386  prjspeclsp  42635  dffltz  42657  diophrw  42782  eldioph2b  42786  diophin  42795  rexrabdioph  42817  jm2.26a  43024  jm2.27  43032  oadif1lem  43403  oadif1  43404  naddgeoa  43418  naddwordnexlem4  43425  suplesup  45366  uzub  45458  supminfxr  45491  infrpgernmpt  45492  limsuppnflem  45739  limsupubuz  45742  climinf3  45745  limsupre3lem  45761  limsupre3uzlem  45764  limsupvaluz2  45767  supcnvlimsup  45769  limsupresxr  45795  liminfresxr  45796  limsupgtlem  45806  liminfvalxr  45812  liminfreuzlem  45831  cnrefiisplem  45858  xlimmnfvlem2  45862  xlimpnfvlem2  45866  stoweidlem61  46090  carageniuncllem2  46551  icoresmbl  46572  hspmbllem2  46656  ovnovollem3  46687  smflimlem2  46801  smflimlem4  46803  smfmullem3  46822  smfinflem  46846  smfliminflem  46859  fsupdm  46871  finfdm  46875  otiunsndisjX  47308  sprsymrelf1lem  47505  fmtnoprmfac2lem1  47580  fmtnofac1  47584  lighneallem2  47620  dfodd6  47651  dfeven4  47652  m1expevenALTV  47661  opoeALTV  47697  opeoALTV  47698  mogoldbb  47799  nnsum4primeseven  47814  grimgrtri  47961  uzlidlring  48210  islindeps2  48459  isldepslvec2  48461  m1modmmod  48501  eenglngeehlnmlem1  48717