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 3054
Description: Restricted quantifier version of 19.29 1789. See also r19.29r 3055. (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 462 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
21ralimi 2936 . . 3 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 (𝜓 → (𝜑𝜓)))
3 rexim 2991 . . 3 (∀𝑥𝐴 (𝜓 → (𝜑𝜓)) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 (𝜑𝜓)))
42, 3syl 17 . 2 (∀𝑥𝐴 𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 (𝜑𝜓)))
54imp 444 1 ((∀𝑥𝐴 𝜑 ∧ ∃𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wral 2896  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902
This theorem is referenced by:  r19.29r  3055  r19.29d2r  3061  disjiun  4573  triun  4694  ralxfrd  4805  ralxfrdOLD  4806  ralxfrd2  4810  elrnmptg  5296  fmpt  6289  fliftfun  6462  fun11iun  7019  omabs  7614  findcard3  8088  r1sdom  8520  tcrank  8630  infxpenlem  8719  dfac12k  8852  cfslb2n  8973  cfcoflem  8977  iundom2g  9241  supsrlem  9811  axpre-sup  9869  fimaxre3  10849  limsupbnd2  14062  rlimuni  14129  rlimcld2  14157  rlimno1  14232  pgpfac1lem5  18301  ppttop  20621  epttop  20623  tgcnp  20867  lmcnp  20918  bwth  21023  1stcrest  21066  txlm  21261  tx1stc  21263  fbfinnfr  21455  fbunfip  21483  filuni  21499  ufileu  21533  fbflim2  21591  flftg  21610  ufilcmp  21646  cnpfcf  21655  tsmsxp  21768  metss  22123  lmmbr  22864  ivthlem2  23028  ivthlem3  23029  dyadmax  23172  rhmdvdsr  29149  tpr2rico  29286  esumpcvgval  29467  sigaclcuni  29508  voliune  29619  volfiniune  29620  dya2icoseg2  29667  poimirlem29  32608  unirep  32677  heibor1lem  32778  2r19.29  33160  pmapglbx  34073  stoweidlem35  38928
  Copyright terms: Public domain W3C validator