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  8123  summolem2  15664  cygabl  19761  dissnlocfin  23040  utopsnneiplem  23759  restmetu  24086  elqaa  25842  2sqmo  26947  colline  27938  axcontlem2  28261  grpoidinvlem4  29798  2ndimaxp  31910  fnpreimac  31934  cyc3genpm  32352  isarchi3  32374  dvdsruasso  32535  grplsmid  32559  quslsm  32561  nsgqusf1olem2  32570  nsgqusf1olem3  32571  ghmquskerlem1  32573  elrspunidl  32591  elrspunsn  32592  ssmxidllem  32634  ist0cld  32882  qtophaus  32885  locfinreflem  32889  cmpcref  32899  ordtconnlem1  32973  esumpcvgval  33145  esumcvg  33153  eulerpartlems  33428  eulerpartlemgvv  33444  reprinfz1  33703  reprpmtf1o  33707  satffunlem2lem2  34466  isbnd3  36738  eldiophss  41594  eldioph4b  41631  pellfund14b  41719  opeoALTV  46431