Theorem r19.29an 3138

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

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

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 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  fimaproj  8117  summolem2  15689  ghmqusnsglem1  19219  ghmquskerlem1  19222  cygabl  19828  dissnlocfin  23423  utopsnneiplem  24142  restmetu  24465  elqaa  26237  2sqmo  27355  colline  28583  axcontlem2  28899  grpoidinvlem4  30443  2ndimaxp  32577  fnpreimac  32602  mndlrinvb  32973  mndlactfo  32975  mndractfo  32977  mndlactf1o  32978  mndractf1o  32979  cyc3genpm  33116  isarchi3  33148  elrgspn  33204  elrgspnsubrun  33207  fracerl  33263  dvdsruasso  33363  dvdsruasso2  33364  grplsmid  33382  quslsm  33383  nsgqusf1olem2  33392  nsgqusf1olem3  33393  elrspunidl  33406  elrspunsn  33407  ssdifidllem  33434  ssdifidlprm  33436  ssmxidllem  33451  1arithidom  33515  1arithufdlem3  33524  fldextrspunlsp  33676  constrconj  33742  constrfin  33743  constrelextdg2  33744  constrfiss  33748  ist0cld  33830  qtophaus  33833  locfinreflem  33837  cmpcref  33847  ordtconnlem1  33921  esumpcvgval  34075  esumcvg  34083  eulerpartlems  34358  eulerpartlemgvv  34374  reprinfz1  34620  reprpmtf1o  34624  satffunlem2lem2  35400  isbnd3  37785  eldiophss  42769  eldioph4b  42806  pellfund14b  42894  opeoALTV  47689