Theorem r19.29an 3137

Description: A commonly used pattern in the spirit of r19.29 3094. (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 3136	. 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  8091  summolem2  15658  ghmqusnsglem1  19188  ghmquskerlem1  19191  cygabl  19797  dissnlocfin  23392  utopsnneiplem  24111  restmetu  24434  elqaa  26206  2sqmo  27324  colline  28552  axcontlem2  28868  grpoidinvlem4  30409  2ndimaxp  32543  fnpreimac  32568  mndlrinvb  32939  mndlactfo  32941  mndractfo  32943  mndlactf1o  32944  mndractf1o  32945  cyc3genpm  33082  isarchi3  33114  elrgspn  33170  elrgspnsubrun  33173  fracerl  33229  dvdsruasso  33329  dvdsruasso2  33330  grplsmid  33348  quslsm  33349  nsgqusf1olem2  33358  nsgqusf1olem3  33359  elrspunidl  33372  elrspunsn  33373  ssdifidllem  33400  ssdifidlprm  33402  ssmxidllem  33417  1arithidom  33481  1arithufdlem3  33490  fldextrspunlsp  33642  constrconj  33708  constrfin  33709  constrelextdg2  33710  constrfiss  33714  ist0cld  33796  qtophaus  33799  locfinreflem  33803  cmpcref  33813  ordtconnlem1  33887  esumpcvgval  34041  esumcvg  34049  eulerpartlems  34324  eulerpartlemgvv  34340  reprinfz1  34586  reprpmtf1o  34590  satffunlem2lem2  35366  isbnd3  37751  eldiophss  42735  eldioph4b  42772  pellfund14b  42860  opeoALTV  47658