Theorem r19.29an 3156

Description: A commonly used pattern in the spirit of r19.29 3112. (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 3155	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
3	2	imp 406	1 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-rex 3069

This theorem is referenced by:  fimaproj  8159  summolem2  15749  ghmqusnsglem1  19311  ghmquskerlem1  19314  cygabl  19924  dissnlocfin  23553  utopsnneiplem  24272  restmetu  24599  elqaa  26379  2sqmo  27496  colline  28672  axcontlem2  28995  grpoidinvlem4  30536  2ndimaxp  32663  fnpreimac  32688  mndlrinvb  33013  mndlactfo  33015  mndractfo  33017  mndlactf1o  33018  mndractf1o  33019  cyc3genpm  33155  isarchi3  33177  fracerl  33288  dvdsruasso  33393  dvdsruasso2  33394  grplsmid  33412  quslsm  33413  nsgqusf1olem2  33422  nsgqusf1olem3  33423  elrspunidl  33436  elrspunsn  33437  ssdifidllem  33464  ssdifidlprm  33466  ssmxidllem  33481  1arithidom  33545  1arithufdlem3  33554  constrconj  33750  constrfin  33751  constrelextdg2  33752  ist0cld  33794  qtophaus  33797  locfinreflem  33801  cmpcref  33811  ordtconnlem1  33885  esumpcvgval  34059  esumcvg  34067  eulerpartlems  34342  eulerpartlemgvv  34358  reprinfz1  34616  reprpmtf1o  34620  satffunlem2lem2  35391  isbnd3  37771  eldiophss  42762  eldioph4b  42799  pellfund14b  42887  opeoALTV  47609