Theorem r19.29an 3165

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  fimaproj  8109  summolem2  15734  ghmqusnsglem1  19311  ghmquskerlem1  19314  cygabl  19922  dissnlocfin  23577  utopsnneiplem  24295  restmetu  24618  elqaa  26374  2sqmo  27489  colline  28806  axcontlem2  29123  grpoidinvlem4  30667  2ndimaxp  32809  fnpreimac  32833  mndlrinvb  33164  mndlactfo  33166  mndractfo  33168  mndlactf1o  33169  mndractf1o  33170  cyc3genpm  33293  isarchi3  33328  elrgspn  33388  elrgspnsubrun  33391  rlocisunit  33418  fracerl  33454  dvdsruasso  33532  dvdsruasso2  33533  grplsmid  33551  quslsm  33552  nsgqusf1olem2  33561  nsgqusf1olem3  33562  elrspunidl  33575  elrspunsn  33576  ssdifidllem  33604  ssdifidlprm  33606  ssmxidllem  33622  1arithidom  33694  1arithufdlem3  33703  fldextrspunlsp  33932  constrconj  34003  constrfin  34004  constrelextdg2  34005  constrfiss  34009  ist0cld  34091  qtophaus  34094  locfinreflem  34098  cmpcref  34108  ordtconnlem1  34182  esumpcvgval  34336  esumcvg  34344  eulerpartlems  34618  eulerpartlemgvv  34634  reprinfz1  34877  reprpmtf1o  34881  satffunlem2lem2  35717  isbnd3  38244  eldiophss  43316  eldioph4b  43349  pellfund14b  43437  opeoALTV  48267