Theorem r19.29an 3166

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

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

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 3087

This theorem is used by:  fimaproj  8133  summolem2  15802  ghmqusnsglem1  19407  ghmquskerlem1  19410  cygabl  20018  ssdifidllem  21547  ssdifidlprm  21549  dissnlocfin  23755  utopsnneiplem  24473  restmetu  24796  elqaa  26554  2sqmo  27673  colline  28997  cgraer  29256  cgrabasimass  29257  angmgmaddcpbl  29269  angmgmaddcl  29270  angmgmaddlid  29271  angmgmaddrid  29272  dfprlng2  29304  axcontlem2  29422  grpoidinvlem4  30988  2ndimaxp  33119  fnpreimac  33143  mndlrinvb  33465  mndlactfo  33467  mndractfo  33469  mndlactf1o  33470  mndractf1o  33471  cyc3genpm  33592  isarchi3  33627  elrgspn  33686  elrgspnsubrun  33689  rlocisunit  33716  fracerl  33747  dvdsruasso  33818  dvdsruasso2  33819  grplsmid  33833  quslsm  33834  nsgqusf1olem2  33843  nsgqusf1olem3  33844  elrspunidl  33856  elrspunsn  33857  ssmxidllem  33876  1arithidom  33947  1arithufdlem3  33956  fldextrspunlsp  34184  constrconj  34255  constrfin  34256  constrelextdg2  34257  constrfiss  34261  ist0cld  34343  qtophaus  34346  locfinreflem  34350  cmpcref  34360  ordtconnlem1  34434  esumpcvgval  34588  esumcvg  34596  eulerpartlems  34871  eulerpartlemgvv  34887  reprinfz1  35130  reprpmtf1o  35134  satffunlem2lem2  35985  isbnd3  38534  eldiophss  43619  eldioph4b  43652  pellfund14b  43740  opeoALTV  48600