Theorem rexlimdva2 3158

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

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 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  r19.29an  3159  r19.29a  3163  otiunsndisj  5519  dffo3  7099  omlimcl  8574  cfflb  10250  cfcof  10265  alephval2  10563  pwcfsdom  10574  recexsr  11098  zdiv  12628  modmuladd  13874  ssnn0fi  13946  2cshwcshw  14772  wrdl3s3  14909  s3iunsndisj  14911  odd2np1  16280  mod2eq1n2dvds  16286  m1expo  16314  dvdsnprmd  16623  ncoprmlnprm  16660  lspsneleq  20716  psgndif  21139  islinds4  21374  cply1coe0bi  21806  mat1dimcrng  21961  smatvscl  22008  cpmatinvcl  22201  pmatcollpw3fi1lem2  22271  fctop  22489  cctop  22491  neindisj  22603  innei  22611  restcld  22658  isnrm3  22845  dis2ndc  22946  fgcl  23364  ufileu  23405  bcthlem5  24827  iundisj  25047  vitalilem2  25108  dcubic  26331  2lgslem1c  26876  2lgslem3a1  26883  2lgslem3b1  26884  2lgslem3c1  26885  2lgslem3d1  26886  f1otrg  28102  umgrnloop  28348  erclwwlkeqlen  29252  erclwwlktr  29255  erclwwlkneqlen  29301  eleclclwwlkn  29309  umgr3v3e3cycl  29417  cusconngr  29424  eucrctshift  29476  2pthfrgr  29517  grpoinvf  29763  nmosetre  29995  blocnilem  30035  shsel3  30546  normcan  30807  nmfnsetre  31108  superpos  31585  iundisjfi  31985  indf1ofs  32962  esumcst  32999  eulerpartlemgh  33315  afsval  33621  fmlasuc  34315  satffunlem2lem2  34335  brsegle2  35019  heicant  36461  itg2gt0cn  36481  sdclem1  36549  sstotbnd3  36582  prtlem10  37673  prjspeclsp  41298  dffltz  41320  diophrw  41430  eldioph2b  41434  diophin  41443  rexrabdioph  41465  jm2.26a  41672  jm2.27  41680  oadif1lem  42062  oadif1  42063  naddgeoa  42078  naddwordnexlem4  42085  suplesup  43984  uzub  44076  supminfxr  44109  infrpgernmpt  44110  limsuppnflem  44361  limsupubuz  44364  climinf3  44367  limsupre3lem  44383  limsupre3uzlem  44386  limsupvaluz2  44389  supcnvlimsup  44391  limsupresxr  44417  liminfresxr  44418  liminflelimsuplem  44426  limsupgtlem  44428  liminfvalxr  44434  liminfreuzlem  44453  cnrefiisplem  44480  xlimmnfvlem2  44484  xlimpnfvlem2  44488  stoweidlem61  44712  carageniuncllem2  45173  icoresmbl  45194  hspmbllem2  45278  ovnovollem3  45309  smflimlem2  45423  smflimlem4  45425  smfmullem3  45444  smfinflem  45468  smfliminflem  45481  fsupdm  45493  finfdm  45497  otiunsndisjX  45922  sprsymrelf1lem  46094  fmtnoprmfac2lem1  46169  fmtnofac1  46173  lighneallem2  46209  dfodd6  46240  dfeven4  46241  m1expevenALTV  46250  opoeALTV  46286  opeoALTV  46287  mogoldbb  46388  nnsum4primeseven  46403  rngqiprngimfo  46715  uzlidlring  46729  islindeps2  47066  isldepslvec2  47068  m1modmmod  47109  eenglngeehlnmlem1  47325