Theorem r19.29an 3164

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  fimaproj  8176  summolem2  15764  ghmqusnsglem1  19320  ghmquskerlem1  19323  cygabl  19933  dissnlocfin  23558  utopsnneiplem  24277  restmetu  24604  elqaa  26382  2sqmo  27499  colline  28675  axcontlem2  28998  grpoidinvlem4  30539  2ndimaxp  32665  fnpreimac  32689  mndlrinvb  33011  mndlactfo  33013  mndractfo  33015  mndlactf1o  33016  mndractf1o  33017  cyc3genpm  33145  isarchi3  33167  fracerl  33273  dvdsruasso  33378  dvdsruasso2  33379  grplsmid  33397  quslsm  33398  nsgqusf1olem2  33407  nsgqusf1olem3  33408  elrspunidl  33421  elrspunsn  33422  ssdifidllem  33449  ssdifidlprm  33451  ssmxidllem  33466  1arithidom  33530  1arithufdlem3  33539  constrconj  33735  constrfin  33736  constrelextdg2  33737  ist0cld  33779  qtophaus  33782  locfinreflem  33786  cmpcref  33796  ordtconnlem1  33870  esumpcvgval  34042  esumcvg  34050  eulerpartlems  34325  eulerpartlemgvv  34341  reprinfz1  34599  reprpmtf1o  34603  satffunlem2lem2  35374  isbnd3  37744  eldiophss  42730  eldioph4b  42767  pellfund14b  42855  opeoALTV  47558