Theorem r19.29an 3141

Description: A commonly used pattern in the spirit of r19.29 3100. (Contributed by Thierry Arnoux, 29-Dec-2019.) (Proof shortened by Wolf Lammen, 17-Jun-2023.)

Hypothesis

Ref	Expression
rexlimdva2.1	⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
r19.29an	⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.29an

Step	Hyp	Ref	Expression
1		rexlimdva2.1	. . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝜓) → 𝜒)
2	1	rexlimdva2 3140	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
3	2	imp 406	1 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  fimaproj  8085  summolem2  15678  ghmqusnsglem1  19255  ghmquskerlem1  19258  cygabl  19866  dissnlocfin  23494  utopsnneiplem  24212  restmetu  24535  elqaa  26288  2sqmo  27400  colline  28717  axcontlem2  29034  grpoidinvlem4  30578  2ndimaxp  32719  fnpreimac  32743  mndlrinvb  33085  mndlactfo  33087  mndractfo  33089  mndlactf1o  33090  mndractf1o  33091  cyc3genpm  33213  isarchi3  33248  elrgspn  33307  elrgspnsubrun  33310  fracerl  33367  dvdsruasso  33445  dvdsruasso2  33446  grplsmid  33464  quslsm  33465  nsgqusf1olem2  33474  nsgqusf1olem3  33475  elrspunidl  33488  elrspunsn  33489  ssdifidllem  33516  ssdifidlprm  33518  ssmxidllem  33533  1arithidom  33597  1arithufdlem3  33606  fldextrspunlsp  33818  constrconj  33889  constrfin  33890  constrelextdg2  33891  constrfiss  33895  ist0cld  33977  qtophaus  33980  locfinreflem  33984  cmpcref  33994  ordtconnlem1  34068  esumpcvgval  34222  esumcvg  34230  eulerpartlems  34504  eulerpartlemgvv  34520  reprinfz1  34766  reprpmtf1o  34770  satffunlem2lem2  35588  isbnd3  38105  eldiophss  43206  eldioph4b  43239  pellfund14b  43327  opeoALTV  48160