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

Theorem r19.29 3252
Description: Restricted quantifier version of 19.29 1867. See also r19.29r 3253. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.29 ((∀𝑥𝐴 𝜑 ∧ ∃𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))

Proof of Theorem r19.29
StepHypRef Expression
1 pm3.2 472 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
21ralimi 3158 . . 3 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 (𝜓 → (𝜑𝜓)))
3 rexim 3239 . . 3 (∀𝑥𝐴 (𝜓 → (𝜑𝜓)) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 (𝜑𝜓)))
42, 3syl 17 . 2 (∀𝑥𝐴 𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 (𝜑𝜓)))
54imp 409 1 ((∀𝑥𝐴 𝜑 ∧ ∃𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wral 3136  wrex 3137
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 209  df-an 399  df-ex 1774  df-ral 3141  df-rex 3142
This theorem is referenced by:  r19.29r  3253  r19.29rOLD  3254  2r19.29  3332  r19.29d2r  3333  disjiun  5044  triun  5176  ralxfrd  5299  ralxfrd2  5303  elrnmptg  5824  fmpt  6867  fliftfun  7057  fiunlem  7635  fiun  7636  f1iun  7637  omabs  8266  findcard3  8753  r1sdom  9195  tcrank  9305  infxpenlem  9431  dfac12k  9565  cfslb2n  9682  cfcoflem  9686  iundom2g  9954  supsrlem  10525  axpre-sup  10583  fimaxre3  11579  hashgt23el  13777  limsupbnd2  14832  rlimuni  14899  rlimcld2  14927  rlimno1  15002  pgpfac1lem5  19193  ppttop  21607  epttop  21609  tgcnp  21853  lmcnp  21904  bwth  22010  1stcrest  22053  txlm  22248  tx1stc  22250  fbfinnfr  22441  fbunfip  22469  filuni  22485  ufileu  22519  fbflim2  22577  flftg  22596  ufilcmp  22632  cnpfcf  22641  tsmsxp  22755  metss  23110  lmmbr  23853  ivthlem2  24045  ivthlem3  24046  dyadmax  24191  rhmdvdsr  30884  tpr2rico  31143  esumpcvgval  31325  sigaclcuni  31365  voliune  31476  volfiniune  31477  dya2icoseg2  31524  umgr2cycllem  32375  umgr2cycl  32376  poimirlem29  34908  unirep  34975  heibor1lem  35074  pmapglbx  36892  stoweidlem35  42305
  Copyright terms: Public domain W3C validator