Theorem r19.29an 3288

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2110  ∃wrex 3139

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 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  fimaproj  7823  summolem2  15067  cygabl  19004  cygablOLD  19005  dissnlocfin  22131  utopsnneiplem  22850  restmetu  23174  elqaa  24905  2sqmo  26007  colline  26429  axcontlem2  26745  grpoidinvlem4  28278  fnpreimac  30410  cyc3genpm  30789  isarchi3  30811  ssmxidllem  30973  qtophaus  31095  locfinreflem  31099  cmpcref  31109  ordtconnlem1  31162  esumpcvgval  31332  esumcvg  31340  eulerpartlems  31613  eulerpartlemgvv  31629  reprinfz1  31888  reprpmtf1o  31892  satffunlem2lem2  32648  isbnd3  35056  eldiophss  39364  eldioph4b  39401  pellfund14b  39489  opeoALTV  43842