Theorem rexlimdva2 3164

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  r19.29an  3165  r19.29a  3169  otiunsndisj  5488  dffo3  7079  omlimcl  8542  cfflb  10213  cfcof  10228  alephval2  10527  pwcfsdom  10538  recexsr  11062  zdiv  12640  modmuladd  13923  ssnn0fi  13995  2cshwcshw  14835  wrdl3s3  14972  s3iunsndisj  14978  odd2np1  16358  mod2eq1n2dvds  16364  m1expo  16392  dvdsnprmd  16707  ncoprmlnprm  16746  lspsneleq  21165  rngqiprngimfo  21351  pzriprnglem4  21516  psgndif  21634  islinds4  21867  cply1coe0bi  22345  mat1dimcrng  22517  smatvscl  22564  cpmatinvcl  22757  pmatcollpw3fi1lem2  22827  fctop  23044  cctop  23046  neindisj  23157  innei  23165  restcld  23212  isnrm3  23399  dis2ndc  23500  fgcl  23918  ufileu  23959  bcthlem5  25370  iundisj  25590  vitalilem2  25651  dcubic  26888  2lgslem1c  27434  2lgslem3a1  27441  2lgslem3b1  27442  2lgslem3c1  27443  2lgslem3d1  27444  f1otrg  29017  umgrnloop  29255  erclwwlkeqlen  30167  erclwwlktr  30170  erclwwlkneqlen  30216  eleclclwwlkn  30224  umgr3v3e3cycl  30332  cusconngr  30339  eucrctshift  30391  2pthfrgr  30432  grpoinvf  30681  nmosetre  30913  blocnilem  30953  shsel3  31464  normcan  31725  nmfnsetre  32026  superpos  32503  iundisjfi  32948  indf1ofs  33005  dfufd2  33707  constrextdg2lem  34006  constrextdg2  34007  esumcst  34321  eulerpartlemgh  34636  afsval  34932  fmlasuc  35700  satffunlem2lem2  35720  brsegle2  36423  heicant  38118  itg2gt0cn  38138  sdclem1  38206  sstotbnd3  38239  prtlem10  39453  zdivgd  42910  prjspeclsp  43158  dffltz  43180  diophrw  43304  eldioph2b  43308  diophin  43317  rexrabdioph  43335  jm2.26a  43541  jm2.27  43549  oadif1lem  43920  oadif1  43921  naddgeoa  43935  naddwordnexlem4  43942  suplesup  45879  uzub  45969  supminfxr  46002  infrpgernmpt  46003  limsuppnflem  46248  limsupubuz  46251  climinf3  46254  limsupre3lem  46270  limsupre3uzlem  46273  limsupvaluz2  46276  supcnvlimsup  46278  limsupresxr  46304  liminfresxr  46305  limsupgtlem  46315  liminfvalxr  46321  liminfreuzlem  46340  cnrefiisplem  46367  xlimmnfvlem2  46371  xlimpnfvlem2  46375  stoweidlem61  46599  carageniuncllem2  47060  icoresmbl  47081  hspmbllem2  47165  ovnovollem3  47196  smflimlem2  47310  smflimlem4  47312  smfmullem3  47331  smfinflem  47355  smfliminflem  47368  fsupdm  47380  finfdm  47384  otiunsndisjX  47837  m1modmmod  47922  sprsymrelf1lem  48061  fmtnoprmfac2lem1  48139  fmtnofac1  48143  lighneallem2  48179  dfodd6  48223  dfeven4  48224  m1expevenALTV  48233  opoeALTV  48269  opeoALTV  48270  mogoldbb  48371  nnsum4primeseven  48386  grimgrtri  48535  uzlidlring  48821  islindeps2  49069  isldepslvec2  49071  eenglngeehlnmlem1  49323