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

Theorem r19.29r 3102
 Description: Restricted quantifier version of 19.29r 1842; variation of r19.29 3101. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
r19.29r ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))

Proof of Theorem r19.29r
StepHypRef Expression
1 r19.29 3101 . 2 ((∀𝑥𝐴 𝜓 ∧ ∃𝑥𝐴 𝜑) → ∃𝑥𝐴 (𝜓𝜑))
2 ancom 465 . 2 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) ↔ (∀𝑥𝐴 𝜓 ∧ ∃𝑥𝐴 𝜑))
3 ancom 465 . . 3 ((𝜑𝜓) ↔ (𝜓𝜑))
43rexbii 3070 . 2 (∃𝑥𝐴 (𝜑𝜓) ↔ ∃𝑥𝐴 (𝜓𝜑))
51, 2, 43imtr4i 281 1 ((∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∀wral 2941  ∃wrex 2942 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947 This theorem is referenced by:  r19.29imd  3103  2reu5  3449  rlimuni  14325  rlimno1  14428  neindisj2  20975  lmss  21150  fclsbas  21872  isfcf  21885  ucnima  22132  metcnp3  22392  cfilucfil  22411  bndth  22804  ellimc3  23688  lmxrge0  30126  gsumesum  30249  esumcst  30253  esumfsup  30260  voliune  30420  volfiniune  30421  bnj517  31081  cover2  33638  prmunb2  38827
 Copyright terms: Public domain W3C validator