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

Theorem r19.29 2989
Description: Restricted quantifier version of 19.29 1688. See also r19.29r 2990. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.29  |-  ( ( A. x  e.  A  ph 
/\  E. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )

Proof of Theorem r19.29
StepHypRef Expression
1 pm3.2 445 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21ralimi 2847 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2919 . . 3  |-  ( A. x  e.  A  ( ps  ->  ( ph  /\  ps ) )  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
42, 3syl 16 . 2  |-  ( A. x  e.  A  ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
54imp 427 1  |-  ( ( A. x  e.  A  ph 
/\  E. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   A.wral 2804   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810
This theorem is referenced by:  r19.29r  2990  r19.29d2r  2997  disjiun  4430  triun  4545  ralxfrd  4651  elrnmptg  5241  fmpt  6028  fliftfun  6185  fun11iun  6733  omabs  7288  findcard3  7755  r1sdom  8183  tcrank  8293  infxpenlem  8382  dfac12k  8518  cfslb2n  8639  cfcoflem  8643  iundom2g  8906  supsrlem  9477  axpre-sup  9535  fimaxre3  10487  limsupbnd2  13391  rlimuni  13458  rlimcld2  13486  rlimno1  13561  pgpfac1lem5  17328  ppttop  19678  epttop  19680  tgcnp  19924  lmcnp  19975  bwth  20080  1stcrest  20123  txlm  20318  tx1stc  20320  fbfinnfr  20511  fbunfip  20539  filuni  20555  ufileu  20589  fbflim2  20647  flftg  20666  ufilcmp  20702  cnpfcf  20711  tsmsxp  20826  metss  21180  lmmbr  21866  ivthlem2  22033  ivthlem3  22034  dyadmax  22176  rhmdvdsr  28046  tpr2rico  28132  esumpcvgval  28310  sigaclcuni  28351  voliune  28441  volfiniune  28442  dya2icoseg2  28489  unirep  30446  heibor1lem  30548  2r19.29  30838  stoweidlem35  32059  ralxfrd2  32696  pmapglbx  35909
  Copyright terms: Public domain W3C validator