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

Theorem r19.29 2782
Description: Theorem 19.29 of [Margaris] p. 90 with restricted quantifiers. (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 435 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21ralimi 2717 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2746 . . 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 419 1  |-  ( ( A. x  e.  A  ph 
/\  E. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wral 2642   E.wrex 2643
This theorem is referenced by:  r19.29r  2783  r19.29d2r  2787  disjiun  4136  triun  4249  ralxfrd  4670  elrnmptg  5053  fun11iun  5628  fmpt  5822  fliftfun  5966  omabs  6819  findcard3  7279  r1sdom  7626  tcrank  7734  infxpenlem  7821  dfac12k  7953  cfslb2n  8074  cfcoflem  8078  iundom2g  8341  gruiun  8600  supsrlem  8912  axpre-sup  8970  fimaxre3  9882  limsupbnd2  12197  rlimuni  12264  rlimcld2  12292  rlimno1  12367  pgpfac1lem5  15557  ppttop  16987  epttop  16989  tgcnp  17232  lmcnp  17283  1stcrest  17430  txlm  17594  tx1stc  17596  fbfinnfr  17787  fbunfip  17815  filuni  17831  ufileu  17865  fbflim2  17923  flftg  17942  ufilcmp  17978  cnpfcf  17987  tsmsxp  18098  metss  18421  lmmbr  19075  ivthlem2  19209  ivthlem3  19210  dyadmax  19350  rhmdvdsr  24065  tpr2rico  24107  esumpcvgval  24257  sigaclcuni  24290  voliune  24372  volfiniune  24373  dya2icoseg2  24415  unirep  26098  heibor1lem  26202  2r19.29  26387  stoweidlem35  27445  pmapglbx  29934
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-ral 2647  df-rex 2648
  Copyright terms: Public domain W3C validator