Theorem r19.29an 3170

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  fimaproj  8189  summolem2  15926  ghmqusnsglem1  19545  ghmquskerlem1  19548  cygabl  20156  ssdifidllem  21691  ssdifidlprm  21693  dissnlocfin  23903  utopsnneiplem  24621  restmetu  24944  elqaa  26702  2sqmo  27821  colline  29175  cgraer  29434  cgrabasimass  29435  angmgmaddcpbl  29447  angmgmaddcl  29448  angmgmaddlid  29449  angmgmaddrid  29450  dfprlng2  29482  axcontlem2  29600  grpoidinvlem4  31166  2ndimaxp  33338  fnpreimac  33362  mndlrinvb  33685  mndlactfo  33687  mndractfo  33689  mndlactf1o  33690  mndractf1o  33691  cyc3genpm  33812  isarchi3  33847  elrgspn  33906  elrgspnsubrun  33909  rlocisunit  33936  fracerl  33972  dvdsruasso  34044  dvdsruasso2  34045  grplsmid  34059  quslsm  34060  nsgqusf1olem2  34069  nsgqusf1olem3  34070  elrspunidl  34082  elrspunsn  34083  ssmxidllem  34102  1arithidom  34173  1arithufdlem3  34182  fldextrspunlsp  34417  constrconj  34488  constrfin  34489  constrelextdg2  34490  constrfiss  34494  ist0cld  34576  qtophaus  34579  locfinreflem  34583  cmpcref  34593  ordtconnlem1  34667  esumpcvgval  34821  esumcvg  34829  eulerpartlems  35103  eulerpartlemgvv  35119  reprinfz1  35362  reprpmtf1o  35366  satffunlem2lem2  36379  isbnd3  38984  eldiophss  44051  eldioph4b  44084  pellfund14b  44172  opeoALTV  49055