Theorem r19.29an 3218

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-ral 3070  df-rex 3071

This theorem is referenced by:  fimaproj  7960  summolem2  15409  cygabl  19472  cygablOLD  19473  dissnlocfin  22661  utopsnneiplem  23380  restmetu  23707  elqaa  25463  2sqmo  26566  colline  26991  axcontlem2  27314  grpoidinvlem4  28848  2ndimaxp  30963  fnpreimac  30987  cyc3genpm  31398  isarchi3  31420  grplsmid  31571  quslsm  31572  nsgqusf1olem2  31578  nsgqusf1olem3  31579  elrspunidl  31585  ssmxidllem  31620  ist0cld  31762  qtophaus  31765  locfinreflem  31769  cmpcref  31779  ordtconnlem1  31853  esumpcvgval  32025  esumcvg  32033  eulerpartlems  32306  eulerpartlemgvv  32322  reprinfz1  32581  reprpmtf1o  32585  satffunlem2lem2  33347  isbnd3  35921  eldiophss  40576  eldioph4b  40613  pellfund14b  40701  opeoALTV  45088