Theorem rexlimdva2 3147

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3061

This theorem is referenced by:  r19.29an  3148  r19.29a  3152  otiunsndisj  5516  dffo3  7106  omlimcl  8595  cfflb  10280  cfcof  10295  alephval2  10593  pwcfsdom  10604  recexsr  11128  zdiv  12660  modmuladd  13908  ssnn0fi  13980  2cshwcshw  14806  wrdl3s3  14943  s3iunsndisj  14945  odd2np1  16315  mod2eq1n2dvds  16321  m1expo  16349  dvdsnprmd  16658  ncoprmlnprm  16697  lspsneleq  21005  rngqiprngimfo  21193  pzriprnglem4  21412  psgndif  21536  islinds4  21771  cply1coe0bi  22228  mat1dimcrng  22395  smatvscl  22442  cpmatinvcl  22635  pmatcollpw3fi1lem2  22705  fctop  22923  cctop  22925  neindisj  23037  innei  23045  restcld  23092  isnrm3  23279  dis2ndc  23380  fgcl  23798  ufileu  23839  bcthlem5  25272  iundisj  25493  vitalilem2  25554  dcubic  26794  2lgslem1c  27342  2lgslem3a1  27349  2lgslem3b1  27350  2lgslem3c1  27351  2lgslem3d1  27352  f1otrg  28717  umgrnloop  28963  erclwwlkeqlen  29871  erclwwlktr  29874  erclwwlkneqlen  29920  eleclclwwlkn  29928  umgr3v3e3cycl  30036  cusconngr  30043  eucrctshift  30095  2pthfrgr  30136  grpoinvf  30384  nmosetre  30616  blocnilem  30656  shsel3  31167  normcan  31428  nmfnsetre  31729  superpos  32206  iundisjfi  32607  indf1ofs  33701  esumcst  33738  eulerpartlemgh  34054  afsval  34359  fmlasuc  35052  satffunlem2lem2  35072  brsegle2  35761  heicant  37184  itg2gt0cn  37204  sdclem1  37272  sstotbnd3  37305  prtlem10  38392  zdivgd  41971  prjspeclsp  42100  dffltz  42122  diophrw  42243  eldioph2b  42247  diophin  42256  rexrabdioph  42278  jm2.26a  42485  jm2.27  42493  oadif1lem  42872  oadif1  42873  naddgeoa  42888  naddwordnexlem4  42895  suplesup  44783  uzub  44875  supminfxr  44908  infrpgernmpt  44909  limsuppnflem  45160  limsupubuz  45163  climinf3  45166  limsupre3lem  45182  limsupre3uzlem  45185  limsupvaluz2  45188  supcnvlimsup  45190  limsupresxr  45216  liminfresxr  45217  liminflelimsuplem  45225  limsupgtlem  45227  liminfvalxr  45233  liminfreuzlem  45252  cnrefiisplem  45279  xlimmnfvlem2  45283  xlimpnfvlem2  45287  stoweidlem61  45511  carageniuncllem2  45972  icoresmbl  45993  hspmbllem2  46077  ovnovollem3  46108  smflimlem2  46222  smflimlem4  46224  smfmullem3  46243  smfinflem  46267  smfliminflem  46280  fsupdm  46292  finfdm  46296  otiunsndisjX  46721  sprsymrelf1lem  46893  fmtnoprmfac2lem1  46968  fmtnofac1  46972  lighneallem2  47008  dfodd6  47039  dfeven4  47040  m1expevenALTV  47049  opoeALTV  47085  opeoALTV  47086  mogoldbb  47187  nnsum4primeseven  47202  uzlidlring  47408  islindeps2  47662  isldepslvec2  47664  m1modmmod  47705  eenglngeehlnmlem1  47921