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 3070
Description: Restricted quantifier version of 19.29 1800. See also r19.29r 3071. (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 463 . . . 4 (𝜑 → (𝜓 → (𝜑𝜓)))
21ralimi 2952 . . 3 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 (𝜓 → (𝜑𝜓)))
3 rexim 3007 . . 3 (∀𝑥𝐴 (𝜓 → (𝜑𝜓)) → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 (𝜑𝜓)))
42, 3syl 17 . 2 (∀𝑥𝐴 𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐴 (𝜑𝜓)))
54imp 445 1 ((∀𝑥𝐴 𝜑 ∧ ∃𝑥𝐴 𝜓) → ∃𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wral 2912  wrex 2913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2917  df-rex 2918
This theorem is referenced by:  r19.29r  3071  r19.29d2r  3077  disjiun  4608  triun  4731  ralxfrd  4844  ralxfrdOLD  4845  ralxfrd2  4849  elrnmptg  5339  fmpt  6338  fliftfun  6517  fun11iun  7076  omabs  7673  findcard3  8148  r1sdom  8582  tcrank  8692  infxpenlem  8781  dfac12k  8914  cfslb2n  9035  cfcoflem  9039  iundom2g  9307  supsrlem  9877  axpre-sup  9935  fimaxre3  10915  limsupbnd2  14143  rlimuni  14210  rlimcld2  14238  rlimno1  14313  pgpfac1lem5  18394  ppttop  20716  epttop  20718  tgcnp  20962  lmcnp  21013  bwth  21118  1stcrest  21161  txlm  21356  tx1stc  21358  fbfinnfr  21550  fbunfip  21578  filuni  21594  ufileu  21628  fbflim2  21686  flftg  21705  ufilcmp  21741  cnpfcf  21750  tsmsxp  21863  metss  22218  lmmbr  22959  ivthlem2  23123  ivthlem3  23124  dyadmax  23267  rhmdvdsr  29595  tpr2rico  29732  esumpcvgval  29913  sigaclcuni  29954  voliune  30065  volfiniune  30066  dya2icoseg2  30113  poimirlem29  33056  unirep  33125  heibor1lem  33226  2r19.29  33608  pmapglbx  34521  stoweidlem35  39546
  Copyright terms: Public domain W3C validator