Theorem r19.29an 3159

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  fimaproj  8121  summolem2  15662  cygabl  19759  dissnlocfin  23033  utopsnneiplem  23752  restmetu  24079  elqaa  25835  2sqmo  26940  colline  27900  axcontlem2  28223  grpoidinvlem4  29760  2ndimaxp  31872  fnpreimac  31896  cyc3genpm  32311  isarchi3  32333  dvdsruasso  32490  grplsmid  32514  quslsm  32516  nsgqusf1olem2  32525  nsgqusf1olem3  32526  ghmquskerlem1  32528  elrspunidl  32546  elrspunsn  32547  ssmxidllem  32589  ist0cld  32813  qtophaus  32816  locfinreflem  32820  cmpcref  32830  ordtconnlem1  32904  esumpcvgval  33076  esumcvg  33084  eulerpartlems  33359  eulerpartlemgvv  33375  reprinfz1  33634  reprpmtf1o  33638  satffunlem2lem2  34397  isbnd3  36652  eldiophss  41512  eldioph4b  41549  pellfund14b  41637  opeoALTV  46352