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  5460  dffo3  7035  omlimcl  8493  cfflb  10150  cfcof  10165  alephval2  10463  pwcfsdom  10474  recexsr  10998  zdiv  12543  modmuladd  13820  ssnn0fi  13892  2cshwcshw  14732  wrdl3s3  14869  s3iunsndisj  14875  odd2np1  16252  mod2eq1n2dvds  16258  m1expo  16286  dvdsnprmd  16601  ncoprmlnprm  16639  lspsneleq  21053  rngqiprngimfo  21239  pzriprnglem4  21422  psgndif  21540  islinds4  21773  cply1coe0bi  22218  mat1dimcrng  22393  smatvscl  22440  cpmatinvcl  22633  pmatcollpw3fi1lem2  22703  fctop  22920  cctop  22922  neindisj  23033  innei  23041  restcld  23088  isnrm3  23275  dis2ndc  23376  fgcl  23794  ufileu  23835  bcthlem5  25256  iundisj  25477  vitalilem2  25538  dcubic  26784  2lgslem1c  27332  2lgslem3a1  27339  2lgslem3b1  27340  2lgslem3c1  27341  2lgslem3d1  27342  f1otrg  28850  umgrnloop  29087  erclwwlkeqlen  29997  erclwwlktr  30000  erclwwlkneqlen  30046  eleclclwwlkn  30054  umgr3v3e3cycl  30162  cusconngr  30169  eucrctshift  30221  2pthfrgr  30262  grpoinvf  30510  nmosetre  30742  blocnilem  30782  shsel3  31293  normcan  31554  nmfnsetre  31855  superpos  32332  iundisjfi  32776  indf1ofs  32845  dfufd2  33513  constrextdg2lem  33759  constrextdg2  33760  esumcst  34074  eulerpartlemgh  34389  afsval  34682  fmlasuc  35428  satffunlem2lem2  35448  brsegle2  36149  heicant  37701  itg2gt0cn  37721  sdclem1  37789  sstotbnd3  37822  prtlem10  38910  zdivgd  42376  prjspeclsp  42651  dffltz  42673  diophrw  42798  eldioph2b  42802  diophin  42811  rexrabdioph  42833  jm2.26a  43039  jm2.27  43047  oadif1lem  43418  oadif1  43419  naddgeoa  43433  naddwordnexlem4  43440  suplesup  45384  uzub  45475  supminfxr  45508  infrpgernmpt  45509  limsuppnflem  45754  limsupubuz  45757  climinf3  45760  limsupre3lem  45776  limsupre3uzlem  45779  limsupvaluz2  45782  supcnvlimsup  45784  limsupresxr  45810  liminfresxr  45811  limsupgtlem  45821  liminfvalxr  45827  liminfreuzlem  45846  cnrefiisplem  45873  xlimmnfvlem2  45877  xlimpnfvlem2  45881  stoweidlem61  46105  carageniuncllem2  46566  icoresmbl  46587  hspmbllem2  46671  ovnovollem3  46702  smflimlem2  46816  smflimlem4  46818  smfmullem3  46837  smfinflem  46861  smfliminflem  46874  fsupdm  46886  finfdm  46890  otiunsndisjX  47316  m1modmmod  47395  sprsymrelf1lem  47528  fmtnoprmfac2lem1  47603  fmtnofac1  47607  lighneallem2  47643  dfodd6  47674  dfeven4  47675  m1expevenALTV  47684  opoeALTV  47720  opeoALTV  47721  mogoldbb  47822  nnsum4primeseven  47837  grimgrtri  47986  uzlidlring  48272  islindeps2  48521  isldepslvec2  48523  eenglngeehlnmlem1  48775