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 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  r19.29an  3169  r19.29a  3173  otiunsndisj  5505  dffo3  7099  omlimcl  8564  cfflb  10244  cfcof  10259  alephval2  10558  pwcfsdom  10569  recexsr  11093  zdiv  12667  modmuladd  13951  ssnn0fi  14023  2cshwcshw  14864  wrdl3s3  15001  s3iunsndisj  15007  odd2np1  16400  mod2eq1n2dvds  16406  m1expo  16434  dvdsnprmd  16749  ncoprmlnprm  16788  lspsneleq  21220  rngqiprngimfo  21422  pzriprnglem4  21615  psgndif  21733  islinds4  21966  cply1coe0bi  22443  mat1dimcrng  22615  smatvscl  22662  cpmatinvcl  22855  pmatcollpw3fi1lem2  22925  fctop  23142  cctop  23144  neindisj  23255  innei  23263  restcld  23310  isnrm3  23497  dis2ndc  23598  fgcl  24016  ufileu  24057  bcthlem5  25468  iundisj  25688  vitalilem2  25749  dcubic  26992  2lgslem1c  27538  2lgslem3a1  27545  2lgslem3b1  27546  2lgslem3c1  27547  2lgslem3d1  27548  f1otrg  29201  umgrnloop  29439  erclwwlkeqlen  30351  erclwwlktr  30354  erclwwlkneqlen  30400  eleclclwwlkn  30408  umgr3v3e3cycl  30516  cusconngr  30523  eucrctshift  30575  2pthfrgr  30616  grpoinvf  30865  nmosetre  31097  blocnilem  31137  shsel3  31648  normcan  31909  nmfnsetre  32210  superpos  32687  iundisjfi  33122  indf1ofs  33167  dfufd2  33821  constrextdg2lem  34119  constrextdg2  34120  esumcst  34434  eulerpartlemgh  34749  afsval  35042  fmlasuc  35859  satffunlem2lem2  35879  brsegle2  36582  heicant  38287  itg2gt0cn  38307  sdclem1  38375  sstotbnd3  38408  prtlem10  39620  zdivgd  43079  prjspeclsp  43327  dffltz  43349  diophrw  43473  eldioph2b  43477  diophin  43486  rexrabdioph  43504  jm2.26a  43710  jm2.27  43718  oadif1lem  44089  oadif1  44090  naddgeoa  44104  naddwordnexlem4  44111  suplesup  46038  uzub  46128  supminfxr  46161  infrpgernmpt  46162  limsuppnflem  46407  limsupubuz  46410  climinf3  46413  limsupre3lem  46429  limsupre3uzlem  46432  limsupvaluz2  46435  supcnvlimsup  46437  limsupresxr  46463  liminfresxr  46464  limsupgtlem  46474  liminfvalxr  46480  liminfreuzlem  46499  cnrefiisplem  46526  xlimmnfvlem2  46530  xlimpnfvlem2  46534  stoweidlem61  46758  carageniuncllem2  47219  icoresmbl  47240  hspmbllem2  47324  ovnovollem3  47355  smflimlem2  47469  smflimlem4  47471  smfmullem3  47490  smfinflem  47514  smfliminflem  47527  fsupdm  47539  finfdm  47543  otiunsndisjX  47999  m1modmmod  48084  sprsymrelf1lem  48223  fmtnoprmfac2lem1  48301  fmtnofac1  48305  lighneallem2  48341  dfodd6  48385  dfeven4  48386  m1expevenALTV  48395  opoeALTV  48431  opeoALTV  48432  mogoldbb  48533  nnsum4primeseven  48548  grimgrtri  48697  uzlidlring  48983  islindeps2  49246  isldepslvec2  49248  eenglngeehlnmlem1  49500