Theorem rexlimdva2 3151

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098  ∃wrex 3064

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 396  df-ex 1774  df-rex 3065

This theorem is referenced by:  r19.29an  3152  r19.29a  3156  otiunsndisj  5513  dffo3  7097  omlimcl  8579  cfflb  10256  cfcof  10271  alephval2  10569  pwcfsdom  10580  recexsr  11104  zdiv  12636  modmuladd  13884  ssnn0fi  13956  2cshwcshw  14782  wrdl3s3  14919  s3iunsndisj  14921  odd2np1  16291  mod2eq1n2dvds  16297  m1expo  16325  dvdsnprmd  16634  ncoprmlnprm  16673  lspsneleq  20966  rngqiprngimfo  21154  pzriprnglem4  21371  psgndif  21495  islinds4  21730  cply1coe0bi  22176  mat1dimcrng  22334  smatvscl  22381  cpmatinvcl  22574  pmatcollpw3fi1lem2  22644  fctop  22862  cctop  22864  neindisj  22976  innei  22984  restcld  23031  isnrm3  23218  dis2ndc  23319  fgcl  23737  ufileu  23778  bcthlem5  25211  iundisj  25432  vitalilem2  25493  dcubic  26733  2lgslem1c  27281  2lgslem3a1  27288  2lgslem3b1  27289  2lgslem3c1  27290  2lgslem3d1  27291  f1otrg  28630  umgrnloop  28876  erclwwlkeqlen  29781  erclwwlktr  29784  erclwwlkneqlen  29830  eleclclwwlkn  29838  umgr3v3e3cycl  29946  cusconngr  29953  eucrctshift  30005  2pthfrgr  30046  grpoinvf  30294  nmosetre  30526  blocnilem  30566  shsel3  31077  normcan  31338  nmfnsetre  31639  superpos  32116  iundisjfi  32514  indf1ofs  33554  esumcst  33591  eulerpartlemgh  33907  afsval  34212  fmlasuc  34905  satffunlem2lem2  34925  brsegle2  35614  heicant  37036  itg2gt0cn  37056  sdclem1  37124  sstotbnd3  37157  prtlem10  38248  zdivgd  41808  prjspeclsp  41937  dffltz  41959  diophrw  42080  eldioph2b  42084  diophin  42093  rexrabdioph  42115  jm2.26a  42322  jm2.27  42330  oadif1lem  42710  oadif1  42711  naddgeoa  42726  naddwordnexlem4  42733  suplesup  44626  uzub  44718  supminfxr  44751  infrpgernmpt  44752  limsuppnflem  45003  limsupubuz  45006  climinf3  45009  limsupre3lem  45025  limsupre3uzlem  45028  limsupvaluz2  45031  supcnvlimsup  45033  limsupresxr  45059  liminfresxr  45060  liminflelimsuplem  45068  limsupgtlem  45070  liminfvalxr  45076  liminfreuzlem  45095  cnrefiisplem  45122  xlimmnfvlem2  45126  xlimpnfvlem2  45130  stoweidlem61  45354  carageniuncllem2  45815  icoresmbl  45836  hspmbllem2  45920  ovnovollem3  45951  smflimlem2  46065  smflimlem4  46067  smfmullem3  46086  smfinflem  46110  smfliminflem  46123  fsupdm  46135  finfdm  46139  otiunsndisjX  46564  sprsymrelf1lem  46736  fmtnoprmfac2lem1  46811  fmtnofac1  46815  lighneallem2  46851  dfodd6  46882  dfeven4  46883  m1expevenALTV  46892  opoeALTV  46928  opeoALTV  46929  mogoldbb  47030  nnsum4primeseven  47045  uzlidlring  47190  islindeps2  47444  isldepslvec2  47446  m1modmmod  47487  eenglngeehlnmlem1  47703