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

Theorem r19.29r 3252
Description: Restricted quantifier version of 19.29r 1866; variation of r19.29 3251. (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 3251 . . 3 ((∀𝑥𝐴 𝜓 ∧ ∃𝑥𝐴 𝜑) → ∃𝑥𝐴 (𝜓𝜑))
21ancoms 459 . 2 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜓𝜑))
3 pm3.22 460 . . 3 ((𝜓𝜑) → (𝜑𝜓))
43reximi 3240 . 2 (∃𝑥𝐴 (𝜓𝜑) → ∃𝑥𝐴 (𝜑𝜓))
52, 4syl 17 1 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wral 3135  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3140  df-rex 3141
This theorem is referenced by:  r19.29imd  3254  2reu5  3746  rlimuni  14895  rlimno1  14998  neindisj2  21659  lmss  21834  fclsbas  22557  isfcf  22570  ucnima  22817  metcnp3  23077  cfilucfil  23096  bndth  23489  ellimc3  24404  lmxrge0  31094  gsumesum  31217  esumcst  31221  esumfsup  31228  voliune  31387  volfiniune  31388  bnj517  32056  fvineqsneq  34575  cover2  34870  prmunb2  40520
  Copyright terms: Public domain W3C validator