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 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  fimaproj  8158  summolem2  15891  ghmqusnsglem1  19503  ghmquskerlem1  19506  cygabl  20114  ssdifidllem  21649  ssdifidlprm  21651  dissnlocfin  23857  utopsnneiplem  24575  restmetu  24898  elqaa  26654  2sqmo  27773  colline  29127  cgraer  29386  cgrabasimass  29387  angmgmaddcpbl  29399  angmgmaddcl  29400  angmgmaddlid  29401  angmgmaddrid  29402  dfprlng2  29434  axcontlem2  29552  grpoidinvlem4  31118  2ndimaxp  33291  fnpreimac  33315  mndlrinvb  33636  mndlactfo  33638  mndractfo  33640  mndlactf1o  33641  mndractf1o  33642  cyc3genpm  33763  isarchi3  33798  elrgspn  33857  elrgspnsubrun  33860  rlocisunit  33887  fracerl  33918  dvdsruasso  33990  dvdsruasso2  33991  grplsmid  34005  quslsm  34006  nsgqusf1olem2  34015  nsgqusf1olem3  34016  elrspunidl  34028  elrspunsn  34029  ssmxidllem  34048  1arithidom  34119  1arithufdlem3  34128  fldextrspunlsp  34356  constrconj  34427  constrfin  34428  constrelextdg2  34429  constrfiss  34433  ist0cld  34515  qtophaus  34518  locfinreflem  34522  cmpcref  34532  ordtconnlem1  34606  esumpcvgval  34760  esumcvg  34768  eulerpartlems  35042  eulerpartlemgvv  35058  reprinfz1  35301  reprpmtf1o  35305  satffunlem2lem2  36261  isbnd3  38827  eldiophss  43894  eldioph4b  43927  pellfund14b  44015  opeoALTV  48890