Theorem r19.29 3182

Description: Restricted quantifier version of 19.29 1875. See also r19.29r 3183. (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 474	. . . 4 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
2	1	ralimi 3093	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)))
3		rexim 3169	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 → (𝜑 ∧ 𝜓)) → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
4	2, 3	syl 17	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
5	4	imp 411	1 ⊢ ((∀𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 400  ∀wral 3071  ∃wrex 3072

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-ral 3076  df-rex 3077

This theorem is referenced by:  r19.29r  3183  2r19.29  3256  r19.29d2r  3257  disjiun  5020  triun  5152  ralxfrd  5278  ralxfrd2  5282  elrnmptg  5801  fmpt  6866  fliftfun  7060  fiunlem  7648  fiun  7649  f1iun  7650  omabs  8285  findcard3  8787  r1sdom  9229  tcrank  9339  infxpenlem  9466  dfac12k  9600  cfslb2n  9721  cfcoflem  9725  iundom2g  9993  supsrlem  10564  axpre-sup  10622  fimaxre3  11617  hashgt23el  13828  limsupbnd2  14881  rlimuni  14948  rlimcld2  14976  rlimno1  15051  pgpfac1lem5  19262  ppttop  21700  epttop  21702  tgcnp  21946  lmcnp  21997  bwth  22103  1stcrest  22146  txlm  22341  tx1stc  22343  fbfinnfr  22534  fbunfip  22562  filuni  22578  ufileu  22612  fbflim2  22670  flftg  22689  ufilcmp  22725  cnpfcf  22734  tsmsxp  22848  metss  23203  lmmbr  23951  ivthlem2  24145  ivthlem3  24146  dyadmax  24291  rhmdvdsr  31036  tpr2rico  31376  esumpcvgval  31558  sigaclcuni  31598  voliune  31709  volfiniune  31710  dya2icoseg2  31757  umgr2cycllem  32611  umgr2cycl  32612  poimirlem29  35359  unirep  35424  heibor1lem  35520  pmapglbx  37338  stoweidlem35  43036