Theorem rexlimdva2 3216

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  r19.29an  3217  r19.29a  3218  otiunsndisj  5434  dffo3  6978  omlimcl  8409  cfflb  10015  cfcof  10030  alephval2  10328  pwcfsdom  10339  recexsr  10863  zdiv  12390  modmuladd  13633  ssnn0fi  13705  2cshwcshw  14538  wrdl3s3  14677  s3iunsndisj  14679  odd2np1  16050  mod2eq1n2dvds  16056  m1expo  16084  dvdsnprmd  16395  ncoprmlnprm  16432  lspsneleq  20377  psgndif  20807  islinds4  21042  cply1coe0bi  21471  mat1dimcrng  21626  smatvscl  21673  cpmatinvcl  21866  pmatcollpw3fi1lem2  21936  fctop  22154  cctop  22156  neindisj  22268  innei  22276  restcld  22323  isnrm3  22510  dis2ndc  22611  fgcl  23029  ufileu  23070  bcthlem5  24492  iundisj  24712  vitalilem2  24773  dcubic  25996  2lgslem1c  26541  2lgslem3a1  26548  2lgslem3b1  26549  2lgslem3c1  26550  2lgslem3d1  26551  f1otrg  27232  umgrnloop  27478  erclwwlkeqlen  28383  erclwwlktr  28386  erclwwlkneqlen  28432  eleclclwwlkn  28440  umgr3v3e3cycl  28548  cusconngr  28555  eucrctshift  28607  2pthfrgr  28648  grpoinvf  28894  nmosetre  29126  blocnilem  29166  shsel3  29677  normcan  29938  nmfnsetre  30239  superpos  30716  iundisjfi  31117  indf1ofs  31994  esumcst  32031  eulerpartlemgh  32345  afsval  32651  fmlasuc  33348  satffunlem2lem2  33368  brsegle2  34411  heicant  35812  itg2gt0cn  35832  sdclem1  35901  sstotbnd3  35934  prtlem10  36879  prjspeclsp  40451  dffltz  40471  diophrw  40581  eldioph2b  40585  diophin  40594  rexrabdioph  40616  jm2.26a  40822  jm2.27  40830  suplesup  42878  uzub  42971  supminfxr  43004  infrpgernmpt  43005  limsuppnflem  43251  limsupubuz  43254  climinf3  43257  limsupre3lem  43273  limsupre3uzlem  43276  limsupvaluz2  43279  supcnvlimsup  43281  limsupresxr  43307  liminfresxr  43308  liminflelimsuplem  43316  limsupgtlem  43318  liminfvalxr  43324  liminfreuzlem  43343  cnrefiisplem  43370  xlimmnfvlem2  43374  xlimpnfvlem2  43378  stoweidlem61  43602  carageniuncllem2  44060  icoresmbl  44081  hspmbllem2  44165  ovnovollem3  44196  smflimlem2  44307  smflimlem4  44309  smfmullem3  44327  smfinflem  44350  smfliminflem  44363  otiunsndisjX  44771  sprsymrelf1lem  44943  fmtnoprmfac2lem1  45018  fmtnofac1  45022  lighneallem2  45058  dfodd6  45089  dfeven4  45090  m1expevenALTV  45099  opoeALTV  45135  opeoALTV  45136  mogoldbb  45237  nnsum4primeseven  45252  uzlidlring  45487  islindeps2  45824  isldepslvec2  45826  m1modmmod  45867  eenglngeehlnmlem1  46083