Theorem rexlimdva2 3168

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  r19.29an  3169  r19.29a  3173  otiunsndisj  5494  dffo3  7087  omlimcl  8551  cfflb  10231  cfcof  10246  alephval2  10545  pwcfsdom  10556  recexsr  11080  zdiv  12657  modmuladd  13940  ssnn0fi  14012  2cshwcshw  14852  wrdl3s3  14989  s3iunsndisj  14995  odd2np1  16389  mod2eq1n2dvds  16395  m1expo  16423  dvdsnprmd  16738  ncoprmlnprm  16777  lspsneleq  21208  rngqiprngimfo  21403  pzriprnglem4  21594  psgndif  21712  islinds4  21945  cply1coe0bi  22423  mat1dimcrng  22595  smatvscl  22642  cpmatinvcl  22835  pmatcollpw3fi1lem2  22905  fctop  23122  cctop  23124  neindisj  23235  innei  23243  restcld  23290  isnrm3  23477  dis2ndc  23578  fgcl  23996  ufileu  24037  bcthlem5  25448  iundisj  25668  vitalilem2  25729  dcubic  26969  2lgslem1c  27515  2lgslem3a1  27522  2lgslem3b1  27523  2lgslem3c1  27524  2lgslem3d1  27525  f1otrg  29129  umgrnloop  29367  erclwwlkeqlen  30279  erclwwlktr  30282  erclwwlkneqlen  30328  eleclclwwlkn  30336  umgr3v3e3cycl  30444  cusconngr  30451  eucrctshift  30503  2pthfrgr  30544  grpoinvf  30793  nmosetre  31025  blocnilem  31065  shsel3  31576  normcan  31837  nmfnsetre  32138  superpos  32615  iundisjfi  33053  indf1ofs  33099  dfufd2  33757  constrextdg2lem  34055  constrextdg2  34056  esumcst  34370  eulerpartlemgh  34685  afsval  34978  fmlasuc  35749  satffunlem2lem2  35769  brsegle2  36472  heicant  38166  itg2gt0cn  38186  sdclem1  38254  sstotbnd3  38287  prtlem10  39501  zdivgd  42958  prjspeclsp  43206  dffltz  43228  diophrw  43352  eldioph2b  43356  diophin  43365  rexrabdioph  43383  jm2.26a  43589  jm2.27  43597  oadif1lem  43968  oadif1  43969  naddgeoa  43983  naddwordnexlem4  43990  suplesup  45913  uzub  46003  supminfxr  46036  infrpgernmpt  46037  limsuppnflem  46282  limsupubuz  46285  climinf3  46288  limsupre3lem  46304  limsupre3uzlem  46307  limsupvaluz2  46310  supcnvlimsup  46312  limsupresxr  46338  liminfresxr  46339  limsupgtlem  46349  liminfvalxr  46355  liminfreuzlem  46374  cnrefiisplem  46401  xlimmnfvlem2  46405  xlimpnfvlem2  46409  stoweidlem61  46633  carageniuncllem2  47094  icoresmbl  47115  hspmbllem2  47199  ovnovollem3  47230  smflimlem2  47344  smflimlem4  47346  smfmullem3  47365  smfinflem  47389  smfliminflem  47402  fsupdm  47414  finfdm  47418  otiunsndisjX  47871  m1modmmod  47956  sprsymrelf1lem  48095  fmtnoprmfac2lem1  48173  fmtnofac1  48177  lighneallem2  48213  dfodd6  48257  dfeven4  48258  m1expevenALTV  48267  opoeALTV  48303  opeoALTV  48304  mogoldbb  48405  nnsum4primeseven  48420  grimgrtri  48569  uzlidlring  48855  islindeps2  49114  isldepslvec2  49116  eenglngeehlnmlem1  49368