Theorem rexlimdva2 3157

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  r19.29an  3158  r19.29a  3162  otiunsndisj  5520  dffo3  7103  omlimcl  8577  cfflb  10253  cfcof  10268  alephval2  10566  pwcfsdom  10577  recexsr  11101  zdiv  12631  modmuladd  13877  ssnn0fi  13949  2cshwcshw  14775  wrdl3s3  14912  s3iunsndisj  14914  odd2np1  16283  mod2eq1n2dvds  16289  m1expo  16317  dvdsnprmd  16626  ncoprmlnprm  16663  lspsneleq  20727  psgndif  21154  islinds4  21389  cply1coe0bi  21823  mat1dimcrng  21978  smatvscl  22025  cpmatinvcl  22218  pmatcollpw3fi1lem2  22288  fctop  22506  cctop  22508  neindisj  22620  innei  22628  restcld  22675  isnrm3  22862  dis2ndc  22963  fgcl  23381  ufileu  23422  bcthlem5  24844  iundisj  25064  vitalilem2  25125  dcubic  26348  2lgslem1c  26893  2lgslem3a1  26900  2lgslem3b1  26901  2lgslem3c1  26902  2lgslem3d1  26903  f1otrg  28119  umgrnloop  28365  erclwwlkeqlen  29269  erclwwlktr  29272  erclwwlkneqlen  29318  eleclclwwlkn  29326  umgr3v3e3cycl  29434  cusconngr  29441  eucrctshift  29493  2pthfrgr  29534  grpoinvf  29780  nmosetre  30012  blocnilem  30052  shsel3  30563  normcan  30824  nmfnsetre  31125  superpos  31602  iundisjfi  32002  indf1ofs  33019  esumcst  33056  eulerpartlemgh  33372  afsval  33678  fmlasuc  34372  satffunlem2lem2  34392  brsegle2  35076  heicant  36518  itg2gt0cn  36538  sdclem1  36606  sstotbnd3  36639  prtlem10  37730  prjspeclsp  41355  dffltz  41377  diophrw  41487  eldioph2b  41491  diophin  41500  rexrabdioph  41522  jm2.26a  41729  jm2.27  41737  oadif1lem  42119  oadif1  42120  naddgeoa  42135  naddwordnexlem4  42142  suplesup  44039  uzub  44131  supminfxr  44164  infrpgernmpt  44165  limsuppnflem  44416  limsupubuz  44419  climinf3  44422  limsupre3lem  44438  limsupre3uzlem  44441  limsupvaluz2  44444  supcnvlimsup  44446  limsupresxr  44472  liminfresxr  44473  liminflelimsuplem  44481  limsupgtlem  44483  liminfvalxr  44489  liminfreuzlem  44508  cnrefiisplem  44535  xlimmnfvlem2  44539  xlimpnfvlem2  44543  stoweidlem61  44767  carageniuncllem2  45228  icoresmbl  45249  hspmbllem2  45333  ovnovollem3  45364  smflimlem2  45478  smflimlem4  45480  smfmullem3  45499  smfinflem  45523  smfliminflem  45536  fsupdm  45548  finfdm  45552  otiunsndisjX  45977  sprsymrelf1lem  46149  fmtnoprmfac2lem1  46224  fmtnofac1  46228  lighneallem2  46264  dfodd6  46295  dfeven4  46296  m1expevenALTV  46305  opoeALTV  46341  opeoALTV  46342  mogoldbb  46443  nnsum4primeseven  46458  rngqiprngimfo  46776  pzriprnglem4  46798  uzlidlring  46817  islindeps2  47154  isldepslvec2  47156  m1modmmod  47197  eenglngeehlnmlem1  47413