Theorem r19.29an 3137

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  fimaproj  8114  summolem2  15682  ghmqusnsglem1  19212  ghmquskerlem1  19215  cygabl  19821  dissnlocfin  23416  utopsnneiplem  24135  restmetu  24458  elqaa  26230  2sqmo  27348  colline  28576  axcontlem2  28892  grpoidinvlem4  30436  2ndimaxp  32570  fnpreimac  32595  mndlrinvb  32966  mndlactfo  32968  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  cyc3genpm  33109  isarchi3  33141  elrgspn  33197  elrgspnsubrun  33200  fracerl  33256  dvdsruasso  33356  dvdsruasso2  33357  grplsmid  33375  quslsm  33376  nsgqusf1olem2  33385  nsgqusf1olem3  33386  elrspunidl  33399  elrspunsn  33400  ssdifidllem  33427  ssdifidlprm  33429  ssmxidllem  33444  1arithidom  33508  1arithufdlem3  33517  fldextrspunlsp  33669  constrconj  33735  constrfin  33736  constrelextdg2  33737  constrfiss  33741  ist0cld  33823  qtophaus  33826  locfinreflem  33830  cmpcref  33840  ordtconnlem1  33914  esumpcvgval  34068  esumcvg  34076  eulerpartlems  34351  eulerpartlemgvv  34367  reprinfz1  34613  reprpmtf1o  34617  satffunlem2lem2  35393  isbnd3  37778  eldiophss  42762  eldioph4b  42799  pellfund14b  42887  opeoALTV  47685