Theorem r19.29an 3138

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3059

This theorem is referenced by:  fimaproj  8075  summolem2  15637  ghmqusnsglem1  19207  ghmquskerlem1  19210  cygabl  19818  dissnlocfin  23471  utopsnneiplem  24189  restmetu  24512  elqaa  26284  2sqmo  27402  colline  28670  axcontlem2  28987  grpoidinvlem4  30531  2ndimaxp  32673  fnpreimac  32698  mndlrinvb  33056  mndlactfo  33058  mndractfo  33060  mndlactf1o  33061  mndractf1o  33062  cyc3genpm  33183  isarchi3  33218  elrgspn  33277  elrgspnsubrun  33280  fracerl  33337  dvdsruasso  33415  dvdsruasso2  33416  grplsmid  33434  quslsm  33435  nsgqusf1olem2  33444  nsgqusf1olem3  33445  elrspunidl  33458  elrspunsn  33459  ssdifidllem  33486  ssdifidlprm  33488  ssmxidllem  33503  1arithidom  33567  1arithufdlem3  33576  fldextrspunlsp  33780  constrconj  33851  constrfin  33852  constrelextdg2  33853  constrfiss  33857  ist0cld  33939  qtophaus  33942  locfinreflem  33946  cmpcref  33956  ordtconnlem1  34030  esumpcvgval  34184  esumcvg  34192  eulerpartlems  34466  eulerpartlemgvv  34482  reprinfz1  34728  reprpmtf1o  34732  satffunlem2lem2  35549  isbnd3  37924  eldiophss  42958  eldioph4b  42995  pellfund14b  43083  opeoALTV  47872