Theorem r19.29an 3152

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2104  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-rex 3072

This theorem is referenced by:  fimaproj  8007  summolem2  15473  cygabl  19536  cygablOLD  19537  dissnlocfin  22725  utopsnneiplem  23444  restmetu  23771  elqaa  25527  2sqmo  26630  colline  27055  axcontlem2  27378  grpoidinvlem4  28914  2ndimaxp  31029  fnpreimac  31053  cyc3genpm  31464  isarchi3  31486  grplsmid  31637  quslsm  31638  nsgqusf1olem2  31644  nsgqusf1olem3  31645  elrspunidl  31651  ssmxidllem  31686  ist0cld  31828  qtophaus  31831  locfinreflem  31835  cmpcref  31845  ordtconnlem1  31919  esumpcvgval  32091  esumcvg  32099  eulerpartlems  32372  eulerpartlemgvv  32388  reprinfz1  32647  reprpmtf1o  32651  satffunlem2lem2  33413  isbnd3  35986  eldiophss  40633  eldioph4b  40670  pellfund14b  40758  opeoALTV  45194