Theorem r19.29an 3142

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  fimaproj  8087  summolem2  15651  ghmqusnsglem1  19221  ghmquskerlem1  19224  cygabl  19832  dissnlocfin  23485  utopsnneiplem  24203  restmetu  24526  elqaa  26298  2sqmo  27416  colline  28733  axcontlem2  29050  grpoidinvlem4  30595  2ndimaxp  32736  fnpreimac  32760  mndlrinvb  33118  mndlactfo  33120  mndractfo  33122  mndlactf1o  33123  mndractf1o  33124  cyc3genpm  33246  isarchi3  33281  elrgspn  33340  elrgspnsubrun  33343  fracerl  33400  dvdsruasso  33478  dvdsruasso2  33479  grplsmid  33497  quslsm  33498  nsgqusf1olem2  33507  nsgqusf1olem3  33508  elrspunidl  33521  elrspunsn  33522  ssdifidllem  33549  ssdifidlprm  33551  ssmxidllem  33566  1arithidom  33630  1arithufdlem3  33639  fldextrspunlsp  33852  constrconj  33923  constrfin  33924  constrelextdg2  33925  constrfiss  33929  ist0cld  34011  qtophaus  34014  locfinreflem  34018  cmpcref  34028  ordtconnlem1  34102  esumpcvgval  34256  esumcvg  34264  eulerpartlems  34538  eulerpartlemgvv  34554  reprinfz1  34800  reprpmtf1o  34804  satffunlem2lem2  35622  isbnd3  38035  eldiophss  43131  eldioph4b  43168  pellfund14b  43256  opeoALTV  48044