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

Theorem r19.29 2683
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 434 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21ralimi 2618 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2647 . . 3  |-  ( A. x  e.  A  ( ps  ->  ( ph  /\  ps ) )  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
42, 3syl 15 . 2  |-  ( A. x  e.  A  ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
54imp 418 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 358   A.wral 2543   E.wrex 2544
This theorem is referenced by:  r19.29r  2684  disjiun  4013  triun  4126  ralxfrd  4548  elrnmptg  4929  fun11iun  5493  fmpt  5681  fliftfun  5811  omabs  6645  findcard3  7100  r1sdom  7446  tcrank  7554  infxpenlem  7641  dfac12k  7773  cfslb2n  7894  cfcoflem  7898  iundom2g  8162  gruiun  8421  supsrlem  8733  axpre-sup  8791  fimaxre3  9703  limsupbnd2  11957  rlimuni  12024  rlimcld2  12052  rlimno1  12127  pgpfac1lem5  15314  ppttop  16744  epttop  16746  tgcnp  16983  lmcnp  17032  1stcrest  17179  txlm  17342  tx1stc  17344  fbfinnfr  17536  fbunfip  17564  filuni  17580  ufileu  17614  fbflim2  17672  flftg  17691  ufilcmp  17727  cnpfcf  17736  tsmsxp  17837  metss  18054  lmmbr  18684  ivthlem2  18812  ivthlem3  18813  dyadmax  18953  fordisxex  24366  eqfnung2  24530  intopcoaconlem3b  24950  intopcoaconb  24952  unirep  25761  heibor1lem  25945  2r19.29  26132  stoweidlem35  27196  pmapglbx  29331
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator