Theorem rexlimdva2 3135

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  r19.29an  3136  r19.29a  3140  otiunsndisj  5463  dffo3  7041  omlimcl  8499  cfflb  10156  cfcof  10171  alephval2  10469  pwcfsdom  10480  recexsr  11004  zdiv  12549  modmuladd  13826  ssnn0fi  13898  2cshwcshw  14738  wrdl3s3  14875  s3iunsndisj  14881  odd2np1  16258  mod2eq1n2dvds  16264  m1expo  16292  dvdsnprmd  16607  ncoprmlnprm  16645  lspsneleq  21058  rngqiprngimfo  21244  pzriprnglem4  21427  psgndif  21545  islinds4  21778  cply1coe0bi  22223  mat1dimcrng  22398  smatvscl  22445  cpmatinvcl  22638  pmatcollpw3fi1lem2  22708  fctop  22925  cctop  22927  neindisj  23038  innei  23046  restcld  23093  isnrm3  23280  dis2ndc  23381  fgcl  23799  ufileu  23840  bcthlem5  25261  iundisj  25482  vitalilem2  25543  dcubic  26789  2lgslem1c  27337  2lgslem3a1  27344  2lgslem3b1  27345  2lgslem3c1  27346  2lgslem3d1  27347  f1otrg  28855  umgrnloop  29093  erclwwlkeqlen  30006  erclwwlktr  30009  erclwwlkneqlen  30055  eleclclwwlkn  30063  umgr3v3e3cycl  30171  cusconngr  30178  eucrctshift  30230  2pthfrgr  30271  grpoinvf  30519  nmosetre  30751  blocnilem  30791  shsel3  31302  normcan  31563  nmfnsetre  31864  superpos  32341  iundisjfi  32785  indf1ofs  32854  dfufd2  33522  constrextdg2lem  33768  constrextdg2  33769  esumcst  34083  eulerpartlemgh  34398  afsval  34691  fmlasuc  35437  satffunlem2lem2  35457  brsegle2  36160  heicant  37701  itg2gt0cn  37721  sdclem1  37789  sstotbnd3  37822  prtlem10  38970  zdivgd  42436  prjspeclsp  42711  dffltz  42733  diophrw  42857  eldioph2b  42861  diophin  42870  rexrabdioph  42892  jm2.26a  43098  jm2.27  43106  oadif1lem  43477  oadif1  43478  naddgeoa  43492  naddwordnexlem4  43499  suplesup  45443  uzub  45534  supminfxr  45567  infrpgernmpt  45568  limsuppnflem  45813  limsupubuz  45816  climinf3  45819  limsupre3lem  45835  limsupre3uzlem  45838  limsupvaluz2  45841  supcnvlimsup  45843  limsupresxr  45869  liminfresxr  45870  limsupgtlem  45880  liminfvalxr  45886  liminfreuzlem  45905  cnrefiisplem  45932  xlimmnfvlem2  45936  xlimpnfvlem2  45940  stoweidlem61  46164  carageniuncllem2  46625  icoresmbl  46646  hspmbllem2  46730  ovnovollem3  46761  smflimlem2  46875  smflimlem4  46877  smfmullem3  46896  smfinflem  46920  smfliminflem  46933  fsupdm  46945  finfdm  46949  otiunsndisjX  47384  m1modmmod  47463  sprsymrelf1lem  47596  fmtnoprmfac2lem1  47671  fmtnofac1  47675  lighneallem2  47711  dfodd6  47742  dfeven4  47743  m1expevenALTV  47752  opoeALTV  47788  opeoALTV  47789  mogoldbb  47890  nnsum4primeseven  47905  grimgrtri  48054  uzlidlring  48340  islindeps2  48589  isldepslvec2  48591  eenglngeehlnmlem1  48843