Theorem r19.29an 3158

Description: A commonly used pattern in the spirit of r19.29 3114. (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 3157	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
3	2	imp 407	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:  fimaproj  8117  summolem2  15658  cygabl  19753  dissnlocfin  23024  utopsnneiplem  23743  restmetu  24070  elqaa  25826  2sqmo  26929  colline  27889  axcontlem2  28212  grpoidinvlem4  29747  2ndimaxp  31859  fnpreimac  31883  cyc3genpm  32298  isarchi3  32320  dvdsruasso  32478  grplsmid  32502  quslsm  32504  nsgqusf1olem2  32513  nsgqusf1olem3  32514  ghmquskerlem1  32516  elrspunidl  32534  elrspunsn  32535  ssmxidllem  32577  ist0cld  32801  qtophaus  32804  locfinreflem  32808  cmpcref  32818  ordtconnlem1  32892  esumpcvgval  33064  esumcvg  33072  eulerpartlems  33347  eulerpartlemgvv  33363  reprinfz1  33622  reprpmtf1o  33626  satffunlem2lem2  34385  isbnd3  36640  eldiophss  41497  eldioph4b  41534  pellfund14b  41622  opeoALTV  46338