Theorem r19.29an 3166

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  fimaproj  8152  summolem2  15882  ghmqusnsglem1  19494  ghmquskerlem1  19497  cygabl  20105  ssdifidllem  21640  ssdifidlprm  21642  dissnlocfin  23848  utopsnneiplem  24566  restmetu  24889  elqaa  26645  2sqmo  27764  colline  29118  cgraer  29377  cgrabasimass  29378  angmgmaddcpbl  29390  angmgmaddcl  29391  angmgmaddlid  29392  angmgmaddrid  29393  dfprlng2  29425  axcontlem2  29543  grpoidinvlem4  31109  2ndimaxp  33282  fnpreimac  33306  mndlrinvb  33628  mndlactfo  33630  mndractfo  33632  mndlactf1o  33633  mndractf1o  33634  cyc3genpm  33755  isarchi3  33790  elrgspn  33849  elrgspnsubrun  33852  rlocisunit  33879  fracerl  33910  dvdsruasso  33982  dvdsruasso2  33983  grplsmid  33997  quslsm  33998  nsgqusf1olem2  34007  nsgqusf1olem3  34008  elrspunidl  34020  elrspunsn  34021  ssmxidllem  34040  1arithidom  34111  1arithufdlem3  34120  fldextrspunlsp  34348  constrconj  34419  constrfin  34420  constrelextdg2  34421  constrfiss  34425  ist0cld  34507  qtophaus  34510  locfinreflem  34514  cmpcref  34524  ordtconnlem1  34598  esumpcvgval  34752  esumcvg  34760  eulerpartlems  35034  eulerpartlemgvv  35050  reprinfz1  35293  reprpmtf1o  35297  satffunlem2lem2  36213  isbnd3  38761  eldiophss  43827  eldioph4b  43860  pellfund14b  43948  opeoALTV  48824