Theorem r19.29an 3175

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  fimaproj  8130  summolem2  15766  ghmqusnsglem1  19349  ghmquskerlem1  19352  cygabl  19960  ssdifidllem  21452  ssdifidlprm  21454  dissnlocfin  23654  utopsnneiplem  24372  restmetu  24695  elqaa  26451  2sqmo  27566  colline  28884  axcontlem2  29255  grpoidinvlem4  30799  2ndimaxp  32931  fnpreimac  32955  mndlrinvb  33285  mndlactfo  33287  mndractfo  33289  mndlactf1o  33290  mndractf1o  33291  cyc3genpm  33412  isarchi3  33447  elrgspn  33506  elrgspnsubrun  33509  rlocisunit  33536  fracerl  33569  dvdsruasso  33641  dvdsruasso2  33642  grplsmid  33656  quslsm  33657  nsgqusf1olem2  33666  nsgqusf1olem3  33667  elrspunidl  33679  elrspunsn  33680  ssmxidllem  33700  1arithidom  33771  1arithufdlem3  33780  fldextrspunlsp  34008  constrconj  34079  constrfin  34080  constrelextdg2  34081  constrfiss  34085  ist0cld  34167  qtophaus  34170  locfinreflem  34174  cmpcref  34184  ordtconnlem1  34258  esumpcvgval  34412  esumcvg  34420  eulerpartlems  34694  eulerpartlemgvv  34710  reprinfz1  34953  reprpmtf1o  34957  satffunlem2lem2  35796  isbnd3  38322  eldiophss  43396  eldioph4b  43429  pellfund14b  43517  opeoALTV  48337