Theorem r19.29an 3197

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  ∃wrex 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3056  df-rex 3057

This theorem is referenced by:  fimaproj  7880  summolem2  15245  cygabl  19229  cygablOLD  19230  dissnlocfin  22380  utopsnneiplem  23099  restmetu  23422  elqaa  25169  2sqmo  26272  colline  26694  axcontlem2  27010  grpoidinvlem4  28542  2ndimaxp  30657  fnpreimac  30682  cyc3genpm  31092  isarchi3  31114  grplsmid  31260  quslsm  31261  nsgqusf1olem2  31267  nsgqusf1olem3  31268  elrspunidl  31274  ssmxidllem  31309  ist0cld  31451  qtophaus  31454  locfinreflem  31458  cmpcref  31468  ordtconnlem1  31542  esumpcvgval  31712  esumcvg  31720  eulerpartlems  31993  eulerpartlemgvv  32009  reprinfz1  32268  reprpmtf1o  32272  satffunlem2lem2  33035  isbnd3  35628  eldiophss  40240  eldioph4b  40277  pellfund14b  40365  opeoALTV  44752