Theorem r19.29an 3140

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  fimaproj  8077  summolem2  15639  ghmqusnsglem1  19209  ghmquskerlem1  19212  cygabl  19820  dissnlocfin  23473  utopsnneiplem  24191  restmetu  24514  elqaa  26286  2sqmo  27404  colline  28721  axcontlem2  29038  grpoidinvlem4  30582  2ndimaxp  32724  fnpreimac  32749  mndlrinvb  33107  mndlactfo  33109  mndractfo  33111  mndlactf1o  33112  mndractf1o  33113  cyc3genpm  33234  isarchi3  33269  elrgspn  33328  elrgspnsubrun  33331  fracerl  33388  dvdsruasso  33466  dvdsruasso2  33467  grplsmid  33485  quslsm  33486  nsgqusf1olem2  33495  nsgqusf1olem3  33496  elrspunidl  33509  elrspunsn  33510  ssdifidllem  33537  ssdifidlprm  33539  ssmxidllem  33554  1arithidom  33618  1arithufdlem3  33627  fldextrspunlsp  33831  constrconj  33902  constrfin  33903  constrelextdg2  33904  constrfiss  33908  ist0cld  33990  qtophaus  33993  locfinreflem  33997  cmpcref  34007  ordtconnlem1  34081  esumpcvgval  34235  esumcvg  34243  eulerpartlems  34517  eulerpartlemgvv  34533  reprinfz1  34779  reprpmtf1o  34783  satffunlem2lem2  35600  isbnd3  37985  eldiophss  43016  eldioph4b  43053  pellfund14b  43141  opeoALTV  47930