Theorem rexlimdva2 3212

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2112  ∃wrex 3072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-ral 3076  df-rex 3077

This theorem is referenced by:  r19.29an  3213  r19.29a  3214  otiunsndisj  5377  dffo3  6857  omlimcl  8212  cfflb  9709  cfcof  9724  alephval2  10022  pwcfsdom  10033  recexsr  10557  zdiv  12081  modmuladd  13320  ssnn0fi  13392  2cshwcshw  14224  wrdl3s3  14363  s3iunsndisj  14365  odd2np1  15732  mod2eq1n2dvds  15738  m1expo  15766  dvdsnprmd  16076  ncoprmlnprm  16113  lspsneleq  19945  psgndif  20357  islinds4  20590  cply1coe0bi  21014  mat1dimcrng  21167  smatvscl  21214  cpmatinvcl  21407  pmatcollpw3fi1lem2  21477  fctop  21694  cctop  21696  neindisj  21807  innei  21815  restcld  21862  isnrm3  22049  dis2ndc  22150  fgcl  22568  ufileu  22609  bcthlem5  24018  iundisj  24238  vitalilem2  24299  dcubic  25521  2lgslem1c  26066  2lgslem3a1  26073  2lgslem3b1  26074  2lgslem3c1  26075  2lgslem3d1  26076  f1otrg  26754  umgrnloop  26990  erclwwlkeqlen  27893  erclwwlktr  27896  erclwwlkneqlen  27942  eleclclwwlkn  27950  umgr3v3e3cycl  28058  cusconngr  28065  eucrctshift  28117  2pthfrgr  28158  grpoinvf  28404  nmosetre  28636  blocnilem  28676  shsel3  29187  normcan  29448  nmfnsetre  29749  superpos  30226  iundisjfi  30631  indf1ofs  31503  esumcst  31540  eulerpartlemgh  31854  afsval  32160  fmlasuc  32854  satffunlem2lem2  32874  trpredtr  33306  brsegle2  33950  heicant  35362  itg2gt0cn  35382  sdclem1  35451  sstotbnd3  35484  prtlem10  36431  prjspeclsp  39938  dffltz  39953  diophrw  40063  eldioph2b  40067  diophin  40076  rexrabdioph  40098  jm2.26a  40304  jm2.27  40312  suplesup  42329  uzub  42424  supminfxr  42459  infrpgernmpt  42460  limsuppnflem  42708  limsupubuz  42711  climinf3  42714  limsupre3lem  42730  limsupre3uzlem  42733  limsupvaluz2  42736  supcnvlimsup  42738  limsupresxr  42764  liminfresxr  42765  liminflelimsuplem  42773  limsupgtlem  42775  liminfvalxr  42781  liminfreuzlem  42800  cnrefiisplem  42827  xlimmnfvlem2  42831  xlimpnfvlem2  42835  stoweidlem61  43059  carageniuncllem2  43517  icoresmbl  43538  hspmbllem2  43622  ovnovollem3  43653  smflimlem2  43761  smflimlem4  43763  smfmullem3  43781  smfinflem  43804  smfliminflem  43817  otiunsndisjX  44193  sprsymrelf1lem  44366  fmtnoprmfac2lem1  44441  fmtnofac1  44445  lighneallem2  44481  dfodd6  44512  dfeven4  44513  m1expevenALTV  44522  opoeALTV  44558  opeoALTV  44559  mogoldbb  44660  nnsum4primeseven  44675  uzlidlring  44910  islindeps2  45247  isldepslvec2  45249  m1modmmod  45290  eenglngeehlnmlem1  45506