Theorem r19.29an 3157

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  fimaproj  8124  summolem2  15667  cygabl  19801  dissnlocfin  23254  utopsnneiplem  23973  restmetu  24300  elqaa  26068  2sqmo  27173  colline  28164  axcontlem2  28487  grpoidinvlem4  30024  2ndimaxp  32136  fnpreimac  32160  cyc3genpm  32578  isarchi3  32600  dvdsruasso  32761  grplsmid  32785  quslsm  32787  nsgqusf1olem2  32796  nsgqusf1olem3  32797  ghmquskerlem1  32799  elrspunidl  32817  elrspunsn  32818  ssmxidllem  32860  ist0cld  33108  qtophaus  33111  locfinreflem  33115  cmpcref  33125  ordtconnlem1  33199  esumpcvgval  33371  esumcvg  33379  eulerpartlems  33654  eulerpartlemgvv  33670  reprinfz1  33929  reprpmtf1o  33933  satffunlem2lem2  34692  isbnd3  36956  eldiophss  41815  eldioph4b  41852  pellfund14b  41940  opeoALTV  46652