Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.29an Structured version   Visualization version   GIF version

Theorem r19.29an 3247
 Description: A commonly used pattern in the spirit of r19.29 3216. (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
StepHypRef Expression
1 rexlimdva2.1 . . 3 (((𝜑𝑥𝐴) ∧ 𝜓) → 𝜒)
21rexlimdva2 3246 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
32imp 410 1 ((𝜑 ∧ ∃𝑥𝐴 𝜓) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112 This theorem is referenced by:  fimaproj  7812  summolem2  15065  cygabl  19003  cygablOLD  19004  dissnlocfin  22134  utopsnneiplem  22853  restmetu  23177  elqaa  24918  2sqmo  26021  colline  26443  axcontlem2  26759  grpoidinvlem4  28290  2ndimaxp  30409  fnpreimac  30434  cyc3genpm  30844  isarchi3  30866  elrspunidl  31014  ssmxidllem  31049  ist0cld  31186  qtophaus  31189  locfinreflem  31193  cmpcref  31203  ordtconnlem1  31277  esumpcvgval  31447  esumcvg  31455  eulerpartlems  31728  eulerpartlemgvv  31744  reprinfz1  32003  reprpmtf1o  32007  satffunlem2lem2  32766  isbnd3  35222  eldiophss  39713  eldioph4b  39750  pellfund14b  39838  opeoALTV  44200
 Copyright terms: Public domain W3C validator