Theorem r19.29an 3133

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

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

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 3054

This theorem is referenced by:  fimaproj  8068  summolem2  15623  ghmqusnsglem1  19159  ghmquskerlem1  19162  cygabl  19770  dissnlocfin  23414  utopsnneiplem  24133  restmetu  24456  elqaa  26228  2sqmo  27346  colline  28594  axcontlem2  28910  grpoidinvlem4  30451  2ndimaxp  32589  fnpreimac  32614  mndlrinvb  32979  mndlactfo  32981  mndractfo  32983  mndlactf1o  32984  mndractf1o  32985  cyc3genpm  33094  isarchi3  33129  elrgspn  33186  elrgspnsubrun  33189  fracerl  33245  dvdsruasso  33322  dvdsruasso2  33323  grplsmid  33341  quslsm  33342  nsgqusf1olem2  33351  nsgqusf1olem3  33352  elrspunidl  33365  elrspunsn  33366  ssdifidllem  33393  ssdifidlprm  33395  ssmxidllem  33410  1arithidom  33474  1arithufdlem3  33483  fldextrspunlsp  33641  constrconj  33712  constrfin  33713  constrelextdg2  33714  constrfiss  33718  ist0cld  33800  qtophaus  33803  locfinreflem  33807  cmpcref  33817  ordtconnlem1  33891  esumpcvgval  34045  esumcvg  34053  eulerpartlems  34328  eulerpartlemgvv  34344  reprinfz1  34590  reprpmtf1o  34594  satffunlem2lem2  35379  isbnd3  37764  eldiophss  42747  eldioph4b  42784  pellfund14b  42872  opeoALTV  47668