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

Theorem r19.29r 3217
 Description: Restricted quantifier version of 19.29r 1875; variation of r19.29 3216. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)
Assertion
Ref Expression
r19.29r ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))

Proof of Theorem r19.29r
StepHypRef Expression
1 r19.29 3216 . . 3 ((∀𝑥𝐴 𝜓 ∧ ∃𝑥𝐴 𝜑) → ∃𝑥𝐴 (𝜓𝜑))
21ancoms 462 . 2 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜓𝜑))
3 pm3.22 463 . . 3 ((𝜓𝜑) → (𝜑𝜓))
43reximi 3206 . 2 (∃𝑥𝐴 (𝜓𝜑) → ∃𝑥𝐴 (𝜑𝜓))
52, 4syl 17 1 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∀wral 3106  ∃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 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:  r19.29imd  3218  2reu5  3697  rlimuni  14902  rlimno1  15005  neindisj2  21738  lmss  21913  fclsbas  22636  isfcf  22649  ucnima  22897  metcnp3  23157  cfilucfil  23176  bndth  23573  ellimc3  24492  lmxrge0  31320  gsumesum  31443  esumcst  31447  esumfsup  31454  voliune  31613  volfiniune  31614  bnj517  32282  nummin  32489  fvineqsneq  34848  cover2  35171  prmunb2  41058
 Copyright terms: Public domain W3C validator