Theorem rexlimdva2 3132

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.29an  3133  r19.29a  3137  otiunsndisj  5467  dffo3  7040  omlimcl  8503  cfflb  10172  cfcof  10187  alephval2  10485  pwcfsdom  10496  recexsr  11020  zdiv  12564  modmuladd  13838  ssnn0fi  13910  2cshwcshw  14750  wrdl3s3  14887  s3iunsndisj  14893  odd2np1  16270  mod2eq1n2dvds  16276  m1expo  16304  dvdsnprmd  16619  ncoprmlnprm  16657  lspsneleq  21040  rngqiprngimfo  21226  pzriprnglem4  21409  psgndif  21527  islinds4  21760  cply1coe0bi  22205  mat1dimcrng  22380  smatvscl  22427  cpmatinvcl  22620  pmatcollpw3fi1lem2  22690  fctop  22907  cctop  22909  neindisj  23020  innei  23028  restcld  23075  isnrm3  23262  dis2ndc  23363  fgcl  23781  ufileu  23822  bcthlem5  25244  iundisj  25465  vitalilem2  25526  dcubic  26772  2lgslem1c  27320  2lgslem3a1  27327  2lgslem3b1  27328  2lgslem3c1  27329  2lgslem3d1  27330  f1otrg  28834  umgrnloop  29071  erclwwlkeqlen  29981  erclwwlktr  29984  erclwwlkneqlen  30030  eleclclwwlkn  30038  umgr3v3e3cycl  30146  cusconngr  30153  eucrctshift  30205  2pthfrgr  30246  grpoinvf  30494  nmosetre  30726  blocnilem  30766  shsel3  31277  normcan  31538  nmfnsetre  31839  superpos  32316  iundisjfi  32752  indf1ofs  32822  dfufd2  33500  constrextdg2lem  33717  constrextdg2  33718  esumcst  34032  eulerpartlemgh  34348  afsval  34641  fmlasuc  35361  satffunlem2lem2  35381  brsegle2  36085  heicant  37637  itg2gt0cn  37657  sdclem1  37725  sstotbnd3  37758  prtlem10  38846  zdivgd  42313  prjspeclsp  42588  dffltz  42610  diophrw  42735  eldioph2b  42739  diophin  42748  rexrabdioph  42770  jm2.26a  42976  jm2.27  42984  oadif1lem  43355  oadif1  43356  naddgeoa  43370  naddwordnexlem4  43377  suplesup  45322  uzub  45414  supminfxr  45447  infrpgernmpt  45448  limsuppnflem  45695  limsupubuz  45698  climinf3  45701  limsupre3lem  45717  limsupre3uzlem  45720  limsupvaluz2  45723  supcnvlimsup  45725  limsupresxr  45751  liminfresxr  45752  limsupgtlem  45762  liminfvalxr  45768  liminfreuzlem  45787  cnrefiisplem  45814  xlimmnfvlem2  45818  xlimpnfvlem2  45822  stoweidlem61  46046  carageniuncllem2  46507  icoresmbl  46528  hspmbllem2  46612  ovnovollem3  46643  smflimlem2  46757  smflimlem4  46759  smfmullem3  46778  smfinflem  46802  smfliminflem  46815  fsupdm  46827  finfdm  46831  otiunsndisjX  47267  m1modmmod  47346  sprsymrelf1lem  47479  fmtnoprmfac2lem1  47554  fmtnofac1  47558  lighneallem2  47594  dfodd6  47625  dfeven4  47626  m1expevenALTV  47635  opoeALTV  47671  opeoALTV  47672  mogoldbb  47773  nnsum4primeseven  47788  grimgrtri  47937  uzlidlring  48223  islindeps2  48472  isldepslvec2  48474  eenglngeehlnmlem1  48726