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 3260
Description: Restricted quantifier version of 19.29r 1868; variation of r19.29 3259. (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 3259 . . 3 ((∀𝑥𝐴 𝜓 ∧ ∃𝑥𝐴 𝜑) → ∃𝑥𝐴 (𝜓𝜑))
21ancoms 459 . 2 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜓𝜑))
3 pm3.22 460 . . 3 ((𝜓𝜑) → (𝜑𝜓))
43reximi 3248 . 2 (∃𝑥𝐴 (𝜓𝜑) → ∃𝑥𝐴 (𝜑𝜓))
52, 4syl 17 1 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wral 3143  wrex 3144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-ral 3148  df-rex 3149
This theorem is referenced by:  r19.29imd  3262  2reu5  3753  rlimuni  14897  rlimno1  15000  neindisj2  21647  lmss  21822  fclsbas  22545  isfcf  22558  ucnima  22805  metcnp3  23065  cfilucfil  23084  bndth  23477  ellimc3  24392  lmxrge0  31081  gsumesum  31204  esumcst  31208  esumfsup  31215  voliune  31374  volfiniune  31375  bnj517  32043  fvineqsneq  34562  cover2  34857  prmunb2  40508
  Copyright terms: Public domain W3C validator