Theorem rexlimdva2 3143

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  r19.29an  3144  r19.29a  3148  otiunsndisj  5468  dffo3  7050  omlimcl  8510  cfflb  10179  cfcof  10194  alephval2  10493  pwcfsdom  10504  recexsr  11028  zdiv  12597  modmuladd  13873  ssnn0fi  13945  2cshwcshw  14785  wrdl3s3  14922  s3iunsndisj  14928  odd2np1  16308  mod2eq1n2dvds  16314  m1expo  16342  dvdsnprmd  16657  ncoprmlnprm  16696  lspsneleq  21115  rngqiprngimfo  21301  pzriprnglem4  21466  psgndif  21584  islinds4  21817  cply1coe0bi  22295  mat1dimcrng  22467  smatvscl  22514  cpmatinvcl  22707  pmatcollpw3fi1lem2  22777  fctop  22994  cctop  22996  neindisj  23107  innei  23115  restcld  23162  isnrm3  23349  dis2ndc  23450  fgcl  23868  ufileu  23909  bcthlem5  25320  iundisj  25540  vitalilem2  25601  dcubic  26835  2lgslem1c  27381  2lgslem3a1  27388  2lgslem3b1  27389  2lgslem3c1  27390  2lgslem3d1  27391  f1otrg  28964  umgrnloop  29202  erclwwlkeqlen  30114  erclwwlktr  30117  erclwwlkneqlen  30163  eleclclwwlkn  30171  umgr3v3e3cycl  30279  cusconngr  30286  eucrctshift  30338  2pthfrgr  30379  grpoinvf  30628  nmosetre  30860  blocnilem  30900  shsel3  31411  normcan  31672  nmfnsetre  31973  superpos  32450  iundisjfi  32895  indf1ofs  32952  dfufd2  33640  constrextdg2lem  33939  constrextdg2  33940  esumcst  34254  eulerpartlemgh  34569  afsval  34862  fmlasuc  35621  satffunlem2lem2  35641  brsegle2  36344  heicant  38029  itg2gt0cn  38049  sdclem1  38117  sstotbnd3  38150  prtlem10  39364  zdivgd  42821  prjspeclsp  43069  dffltz  43091  diophrw  43215  eldioph2b  43219  diophin  43228  rexrabdioph  43246  jm2.26a  43452  jm2.27  43460  oadif1lem  43831  oadif1  43832  naddgeoa  43846  naddwordnexlem4  43853  suplesup  45791  uzub  45881  supminfxr  45914  infrpgernmpt  45915  limsuppnflem  46160  limsupubuz  46163  climinf3  46166  limsupre3lem  46182  limsupre3uzlem  46185  limsupvaluz2  46188  supcnvlimsup  46190  limsupresxr  46216  liminfresxr  46217  limsupgtlem  46227  liminfvalxr  46233  liminfreuzlem  46252  cnrefiisplem  46279  xlimmnfvlem2  46283  xlimpnfvlem2  46287  stoweidlem61  46511  carageniuncllem2  46972  icoresmbl  46993  hspmbllem2  47077  ovnovollem3  47108  smflimlem2  47222  smflimlem4  47224  smfmullem3  47243  smfinflem  47267  smfliminflem  47280  fsupdm  47292  finfdm  47296  otiunsndisjX  47749  m1modmmod  47834  sprsymrelf1lem  47973  fmtnoprmfac2lem1  48051  fmtnofac1  48055  lighneallem2  48091  dfodd6  48135  dfeven4  48136  m1expevenALTV  48145  opoeALTV  48181  opeoALTV  48182  mogoldbb  48283  nnsum4primeseven  48298  grimgrtri  48447  uzlidlring  48733  islindeps2  48981  isldepslvec2  48983  eenglngeehlnmlem1  49235