Theorem r19.29an 3171

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

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

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 3092

This theorem is used by:  fimaproj  8137  summolem2  15790  ghmqusnsglem1  19394  ghmquskerlem1  19397  cygabl  20005  ssdifidllem  21534  ssdifidlprm  21536  dissnlocfin  23737  utopsnneiplem  24455  restmetu  24778  elqaa  26534  2sqmo  27652  colline  28974  dfprlng2  29252  axcontlem2  29370  grpoidinvlem4  30930  2ndimaxp  33062  fnpreimac  33086  mndlrinvb  33409  mndlactfo  33411  mndractfo  33413  mndlactf1o  33414  mndractf1o  33415  cyc3genpm  33536  isarchi3  33571  elrgspn  33630  elrgspnsubrun  33633  rlocisunit  33660  fracerl  33691  dvdsruasso  33762  dvdsruasso2  33763  grplsmid  33777  quslsm  33778  nsgqusf1olem2  33787  nsgqusf1olem3  33788  elrspunidl  33800  elrspunsn  33801  ssmxidllem  33820  1arithidom  33891  1arithufdlem3  33900  fldextrspunlsp  34128  constrconj  34199  constrfin  34200  constrelextdg2  34201  constrfiss  34205  ist0cld  34287  qtophaus  34290  locfinreflem  34294  cmpcref  34304  ordtconnlem1  34378  esumpcvgval  34532  esumcvg  34540  eulerpartlems  34815  eulerpartlemgvv  34831  reprinfz1  35074  reprpmtf1o  35078  satffunlem2lem2  35935  isbnd3  38493  eldiophss  43563  eldioph4b  43596  pellfund14b  43684  opeoALTV  48507