Theorem rexlimdva2 3139

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  r19.29an  3140  r19.29a  3144  otiunsndisj  5468  dffo3  7047  omlimcl  8505  cfflb  10169  cfcof  10184  alephval2  10483  pwcfsdom  10494  recexsr  11018  zdiv  12562  modmuladd  13836  ssnn0fi  13908  2cshwcshw  14748  wrdl3s3  14885  s3iunsndisj  14891  odd2np1  16268  mod2eq1n2dvds  16274  m1expo  16302  dvdsnprmd  16617  ncoprmlnprm  16655  lspsneleq  21070  rngqiprngimfo  21256  pzriprnglem4  21439  psgndif  21557  islinds4  21790  cply1coe0bi  22246  mat1dimcrng  22421  smatvscl  22468  cpmatinvcl  22661  pmatcollpw3fi1lem2  22731  fctop  22948  cctop  22950  neindisj  23061  innei  23069  restcld  23116  isnrm3  23303  dis2ndc  23404  fgcl  23822  ufileu  23863  bcthlem5  25284  iundisj  25505  vitalilem2  25566  dcubic  26812  2lgslem1c  27360  2lgslem3a1  27367  2lgslem3b1  27368  2lgslem3c1  27369  2lgslem3d1  27370  f1otrg  28943  umgrnloop  29181  erclwwlkeqlen  30094  erclwwlktr  30097  erclwwlkneqlen  30143  eleclclwwlkn  30151  umgr3v3e3cycl  30259  cusconngr  30266  eucrctshift  30318  2pthfrgr  30359  grpoinvf  30607  nmosetre  30839  blocnilem  30879  shsel3  31390  normcan  31651  nmfnsetre  31952  superpos  32429  iundisjfi  32876  indf1ofs  32948  dfufd2  33631  constrextdg2lem  33905  constrextdg2  33906  esumcst  34220  eulerpartlemgh  34535  afsval  34828  fmlasuc  35580  satffunlem2lem2  35600  brsegle2  36303  heicant  37852  itg2gt0cn  37872  sdclem1  37940  sstotbnd3  37973  prtlem10  39121  zdivgd  42588  prjspeclsp  42851  dffltz  42873  diophrw  42997  eldioph2b  43001  diophin  43010  rexrabdioph  43032  jm2.26a  43238  jm2.27  43246  oadif1lem  43617  oadif1  43618  naddgeoa  43632  naddwordnexlem4  43639  suplesup  45580  uzub  45671  supminfxr  45704  infrpgernmpt  45705  limsuppnflem  45950  limsupubuz  45953  climinf3  45956  limsupre3lem  45972  limsupre3uzlem  45975  limsupvaluz2  45978  supcnvlimsup  45980  limsupresxr  46006  liminfresxr  46007  limsupgtlem  46017  liminfvalxr  46023  liminfreuzlem  46042  cnrefiisplem  46069  xlimmnfvlem2  46073  xlimpnfvlem2  46077  stoweidlem61  46301  carageniuncllem2  46762  icoresmbl  46783  hspmbllem2  46867  ovnovollem3  46898  smflimlem2  47012  smflimlem4  47014  smfmullem3  47033  smfinflem  47057  smfliminflem  47070  fsupdm  47082  finfdm  47086  otiunsndisjX  47521  m1modmmod  47600  sprsymrelf1lem  47733  fmtnoprmfac2lem1  47808  fmtnofac1  47812  lighneallem2  47848  dfodd6  47879  dfeven4  47880  m1expevenALTV  47889  opoeALTV  47925  opeoALTV  47926  mogoldbb  48027  nnsum4primeseven  48042  grimgrtri  48191  uzlidlring  48477  islindeps2  48725  isldepslvec2  48727  eenglngeehlnmlem1  48979