Theorem r19.29 3216

Description: Restricted quantifier version of 19.29 1874. See also r19.29r 3217. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.)

Assertion

Ref	Expression
r19.29	⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Proof of Theorem r19.29

Step	Hyp	Ref	Expression
1		pm3.2 473	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2	1	ralimi 3128	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)))
3		rexim 3204	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
4	2, 3	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
5	4	imp 410	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 399  ∀wral 3106  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  r19.29r  3217  2r19.29  3290  r19.29d2r  3291  disjiun  5017  triun  5149  ralxfrd  5274  ralxfrd2  5278  elrnmptg  5795  fmpt  6851  fliftfun  7044  fiunlem  7625  fiun  7626  f1iun  7627  omabs  8257  findcard3  8745  r1sdom  9187  tcrank  9297  infxpenlem  9424  dfac12k  9558  cfslb2n  9679  cfcoflem  9683  iundom2g  9951  supsrlem  10522  axpre-sup  10580  fimaxre3  11575  hashgt23el  13781  limsupbnd2  14832  rlimuni  14899  rlimcld2  14927  rlimno1  15002  pgpfac1lem5  19194  ppttop  21612  epttop  21614  tgcnp  21858  lmcnp  21909  bwth  22015  1stcrest  22058  txlm  22253  tx1stc  22255  fbfinnfr  22446  fbunfip  22474  filuni  22490  ufileu  22524  fbflim2  22582  flftg  22601  ufilcmp  22637  cnpfcf  22646  tsmsxp  22760  metss  23115  lmmbr  23862  ivthlem2  24056  ivthlem3  24057  dyadmax  24202  rhmdvdsr  30942  tpr2rico  31265  esumpcvgval  31447  sigaclcuni  31487  voliune  31598  volfiniune  31599  dya2icoseg2  31646  umgr2cycllem  32500  umgr2cycl  32501  poimirlem29  35086  unirep  35151  heibor1lem  35247  pmapglbx  37065  stoweidlem35  42677