Theorem rexlimdva2 3147

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2098  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3061

This theorem is referenced by:  r19.29an  3148  r19.29a  3152  otiunsndisj  5517  dffo3  7105  omlimcl  8592  cfflb  10277  cfcof  10292  alephval2  10590  pwcfsdom  10601  recexsr  11125  zdiv  12657  modmuladd  13905  ssnn0fi  13977  2cshwcshw  14803  wrdl3s3  14940  s3iunsndisj  14942  odd2np1  16312  mod2eq1n2dvds  16318  m1expo  16346  dvdsnprmd  16655  ncoprmlnprm  16694  lspsneleq  21002  rngqiprngimfo  21190  pzriprnglem4  21409  psgndif  21533  islinds4  21768  cply1coe0bi  22225  mat1dimcrng  22392  smatvscl  22439  cpmatinvcl  22632  pmatcollpw3fi1lem2  22702  fctop  22920  cctop  22922  neindisj  23034  innei  23042  restcld  23089  isnrm3  23276  dis2ndc  23377  fgcl  23795  ufileu  23836  bcthlem5  25269  iundisj  25490  vitalilem2  25551  dcubic  26791  2lgslem1c  27339  2lgslem3a1  27346  2lgslem3b1  27347  2lgslem3c1  27348  2lgslem3d1  27349  f1otrg  28714  umgrnloop  28960  erclwwlkeqlen  29868  erclwwlktr  29871  erclwwlkneqlen  29917  eleclclwwlkn  29925  umgr3v3e3cycl  30033  cusconngr  30040  eucrctshift  30092  2pthfrgr  30133  grpoinvf  30381  nmosetre  30613  blocnilem  30653  shsel3  31164  normcan  31425  nmfnsetre  31726  superpos  32203  iundisjfi  32604  indf1ofs  33698  esumcst  33735  eulerpartlemgh  34051  afsval  34356  fmlasuc  35049  satffunlem2lem2  35069  brsegle2  35758  heicant  37181  itg2gt0cn  37201  sdclem1  37269  sstotbnd3  37302  prtlem10  38389  zdivgd  41968  prjspeclsp  42097  dffltz  42119  diophrw  42240  eldioph2b  42244  diophin  42253  rexrabdioph  42275  jm2.26a  42482  jm2.27  42490  oadif1lem  42869  oadif1  42870  naddgeoa  42885  naddwordnexlem4  42892  suplesup  44780  uzub  44872  supminfxr  44905  infrpgernmpt  44906  limsuppnflem  45157  limsupubuz  45160  climinf3  45163  limsupre3lem  45179  limsupre3uzlem  45182  limsupvaluz2  45185  supcnvlimsup  45187  limsupresxr  45213  liminfresxr  45214  liminflelimsuplem  45222  limsupgtlem  45224  liminfvalxr  45230  liminfreuzlem  45249  cnrefiisplem  45276  xlimmnfvlem2  45280  xlimpnfvlem2  45284  stoweidlem61  45508  carageniuncllem2  45969  icoresmbl  45990  hspmbllem2  46074  ovnovollem3  46105  smflimlem2  46219  smflimlem4  46221  smfmullem3  46240  smfinflem  46264  smfliminflem  46277  fsupdm  46289  finfdm  46293  otiunsndisjX  46718  sprsymrelf1lem  46890  fmtnoprmfac2lem1  46965  fmtnofac1  46969  lighneallem2  47005  dfodd6  47036  dfeven4  47037  m1expevenALTV  47046  opoeALTV  47082  opeoALTV  47083  mogoldbb  47184  nnsum4primeseven  47199  uzlidlring  47405  islindeps2  47659  isldepslvec2  47661  m1modmmod  47702  eenglngeehlnmlem1  47918