Theorem r19.29an 3169

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  fimaproj  8127  summolem2  15763  ghmqusnsglem1  19345  ghmquskerlem1  19348  cygabl  19956  ssdifidllem  21484  ssdifidlprm  21486  dissnlocfin  23686  utopsnneiplem  24404  restmetu  24727  elqaa  26483  2sqmo  27601  colline  28923  dfprlng2  29197  axcontlem2  29315  grpoidinvlem4  30859  2ndimaxp  32991  fnpreimac  33015  mndlrinvb  33345  mndlactfo  33347  mndractfo  33349  mndlactf1o  33350  mndractf1o  33351  cyc3genpm  33472  isarchi3  33507  elrgspn  33566  elrgspnsubrun  33569  rlocisunit  33596  fracerl  33627  dvdsruasso  33698  dvdsruasso2  33699  grplsmid  33713  quslsm  33714  nsgqusf1olem2  33723  nsgqusf1olem3  33724  elrspunidl  33736  elrspunsn  33737  ssmxidllem  33756  1arithidom  33827  1arithufdlem3  33836  fldextrspunlsp  34064  constrconj  34135  constrfin  34136  constrelextdg2  34137  constrfiss  34141  ist0cld  34223  qtophaus  34226  locfinreflem  34230  cmpcref  34240  ordtconnlem1  34314  esumpcvgval  34468  esumcvg  34476  eulerpartlems  34750  eulerpartlemgvv  34766  reprinfz1  35009  reprpmtf1o  35013  satffunlem2lem2  35898  isbnd3  38435  eldiophss  43505  eldioph4b  43538  pellfund14b  43626  opeoALTV  48449