Theorem r19.29an 3167

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

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

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 1943

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

This theorem is used by:  fimaproj  8145  summolem2  15875  ghmqusnsglem1  19487  ghmquskerlem1  19490  cygabl  20098  ssdifidllem  21633  ssdifidlprm  21635  dissnlocfin  23841  utopsnneiplem  24559  restmetu  24882  elqaa  26638  2sqmo  27757  colline  29111  cgraer  29370  cgrabasimass  29371  angmgmaddcpbl  29383  angmgmaddcl  29384  angmgmaddlid  29385  angmgmaddrid  29386  dfprlng2  29418  axcontlem2  29536  grpoidinvlem4  31102  2ndimaxp  33233  fnpreimac  33257  mndlrinvb  33579  mndlactfo  33581  mndractfo  33583  mndlactf1o  33584  mndractf1o  33585  cyc3genpm  33706  isarchi3  33741  elrgspn  33800  elrgspnsubrun  33803  rlocisunit  33830  fracerl  33861  dvdsruasso  33933  dvdsruasso2  33934  grplsmid  33948  quslsm  33949  nsgqusf1olem2  33958  nsgqusf1olem3  33959  elrspunidl  33971  elrspunsn  33972  ssmxidllem  33991  1arithidom  34062  1arithufdlem3  34071  fldextrspunlsp  34299  constrconj  34370  constrfin  34371  constrelextdg2  34372  constrfiss  34376  ist0cld  34458  qtophaus  34461  locfinreflem  34465  cmpcref  34475  ordtconnlem1  34549  esumpcvgval  34703  esumcvg  34711  eulerpartlems  34985  eulerpartlemgvv  35001  reprinfz1  35244  reprpmtf1o  35248  satffunlem2lem2  36150  isbnd3  38698  eldiophss  43764  eldioph4b  43797  pellfund14b  43885  opeoALTV  48751