Theorem r19.29an 3136

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 3135	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
3	2	imp 406	1 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  fimaproj  8060  summolem2  15618  ghmqusnsglem1  19187  ghmquskerlem1  19190  cygabl  19798  dissnlocfin  23439  utopsnneiplem  24157  restmetu  24480  elqaa  26252  2sqmo  27370  colline  28622  axcontlem2  28938  grpoidinvlem4  30479  2ndimaxp  32620  fnpreimac  32645  mndlrinvb  32998  mndlactfo  33000  mndractfo  33002  mndlactf1o  33003  mndractf1o  33004  cyc3genpm  33113  isarchi3  33148  elrgspn  33205  elrgspnsubrun  33208  fracerl  33264  dvdsruasso  33342  dvdsruasso2  33343  grplsmid  33361  quslsm  33362  nsgqusf1olem2  33371  nsgqusf1olem3  33372  elrspunidl  33385  elrspunsn  33386  ssdifidllem  33413  ssdifidlprm  33415  ssmxidllem  33430  1arithidom  33494  1arithufdlem3  33503  fldextrspunlsp  33679  constrconj  33750  constrfin  33751  constrelextdg2  33752  constrfiss  33756  ist0cld  33838  qtophaus  33841  locfinreflem  33845  cmpcref  33855  ordtconnlem1  33929  esumpcvgval  34083  esumcvg  34091  eulerpartlems  34365  eulerpartlemgvv  34381  reprinfz1  34627  reprpmtf1o  34631  satffunlem2lem2  35442  isbnd3  37824  eldiophss  42807  eldioph4b  42844  pellfund14b  42932  opeoALTV  47715