Theorem r19.29an 3158

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  fimaproj  8160  summolem2  15752  ghmqusnsglem1  19298  ghmquskerlem1  19301  cygabl  19909  dissnlocfin  23537  utopsnneiplem  24256  restmetu  24583  elqaa  26364  2sqmo  27481  colline  28657  axcontlem2  28980  grpoidinvlem4  30526  2ndimaxp  32656  fnpreimac  32681  mndlrinvb  33030  mndlactfo  33032  mndractfo  33034  mndlactf1o  33035  mndractf1o  33036  cyc3genpm  33172  isarchi3  33194  elrgspn  33250  elrgspnsubrun  33253  fracerl  33308  dvdsruasso  33413  dvdsruasso2  33414  grplsmid  33432  quslsm  33433  nsgqusf1olem2  33442  nsgqusf1olem3  33443  elrspunidl  33456  elrspunsn  33457  ssdifidllem  33484  ssdifidlprm  33486  ssmxidllem  33501  1arithidom  33565  1arithufdlem3  33574  fldextrspunlsp  33724  constrconj  33786  constrfin  33787  constrelextdg2  33788  ist0cld  33832  qtophaus  33835  locfinreflem  33839  cmpcref  33849  ordtconnlem1  33923  esumpcvgval  34079  esumcvg  34087  eulerpartlems  34362  eulerpartlemgvv  34378  reprinfz1  34637  reprpmtf1o  34641  satffunlem2lem2  35411  isbnd3  37791  eldiophss  42785  eldioph4b  42822  pellfund14b  42910  opeoALTV  47671