Theorem r19.29an 3144

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 3143	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
3	2	imp 406	1 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)

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

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 3061

This theorem is referenced by:  fimaproj  8134  summolem2  15732  ghmqusnsglem1  19263  ghmquskerlem1  19266  cygabl  19872  dissnlocfin  23467  utopsnneiplem  24186  restmetu  24509  elqaa  26282  2sqmo  27400  colline  28628  axcontlem2  28944  grpoidinvlem4  30488  2ndimaxp  32624  fnpreimac  32649  mndlrinvb  33020  mndlactfo  33022  mndractfo  33024  mndlactf1o  33025  mndractf1o  33026  cyc3genpm  33163  isarchi3  33185  elrgspn  33241  elrgspnsubrun  33244  fracerl  33300  dvdsruasso  33400  dvdsruasso2  33401  grplsmid  33419  quslsm  33420  nsgqusf1olem2  33429  nsgqusf1olem3  33430  elrspunidl  33443  elrspunsn  33444  ssdifidllem  33471  ssdifidlprm  33473  ssmxidllem  33488  1arithidom  33552  1arithufdlem3  33561  fldextrspunlsp  33715  constrconj  33779  constrfin  33780  constrelextdg2  33781  constrfiss  33785  ist0cld  33864  qtophaus  33867  locfinreflem  33871  cmpcref  33881  ordtconnlem1  33955  esumpcvgval  34109  esumcvg  34117  eulerpartlems  34392  eulerpartlemgvv  34408  reprinfz1  34654  reprpmtf1o  34658  satffunlem2lem2  35428  isbnd3  37808  eldiophss  42797  eldioph4b  42834  pellfund14b  42922  opeoALTV  47698