Theorem r19.29an 3253

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2083  ∃wrex 3108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-ral 3112  df-rex 3113

This theorem is referenced by:  summolem2  14910  cygabl  18736  dissnlocfin  21825  utopsnneiplem  22543  restmetu  22867  elqaa  24598  2sqmo  25699  colline  26121  axcontlem2  26438  grpoidinvlem4  27971  fnpreimac  30102  cyc3genpm  30428  isarchi3  30450  fimaproj  30710  qtophaus  30713  locfinreflem  30717  cmpcref  30727  ordtconnlem1  30780  esumpcvgval  30950  esumcvg  30958  eulerpartlems  31231  eulerpartlemgvv  31247  reprinfz1  31506  reprpmtf1o  31510  satffunlem2lem2  32263  isbnd3  34615  eldiophss  38877  eldioph4b  38914  pellfund14b  39002  opeoALTV  43353