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

Theorem r19.29 2645
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 436 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21ralimi 2580 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2609 . . 3  |-  ( A. x  e.  A  ( ps  ->  ( ph  /\  ps ) )  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
42, 3syl 17 . 2  |-  ( A. x  e.  A  ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
54imp 420 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 6    /\ wa 360   A.wral 2509   E.wrex 2510
This theorem is referenced by:  r19.29r  2646  disjiun  3910  triun  4023  ralxfrd  4439  elrnmptg  4836  fun11iun  5350  fmpt  5533  fliftfun  5663  omabs  6531  findcard3  6985  r1sdom  7330  tcrank  7438  infxpenlem  7525  dfac12k  7657  cfslb2n  7778  cfcoflem  7782  iundom2g  8046  gruiun  8301  supsrlem  8613  axpre-sup  8671  fimaxre3  9583  limsupbnd2  11834  rlimuni  11901  rlimcld2  11929  rlimno1  12004  pgpfac1lem5  15149  ppttop  16576  epttop  16578  tgcnp  16815  lmcnp  16864  1stcrest  17011  txlm  17174  tx1stc  17176  fbfinnfr  17368  fbunfip  17396  filuni  17412  ufileu  17446  fbflim2  17504  flftg  17523  ufilcmp  17559  cnpfcf  17568  tsmsxp  17669  metss  17886  lmmbr  18516  ivthlem2  18644  ivthlem3  18645  dyadmax  18785  fordisxex  24119  eqfnung2  24284  intopcoaconlem3b  24704  intopcoaconb  24706  unirep  25515  heibor1lem  25699  2r19.29  25886  stoweidlem35  26918  pmapglbx  28862
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-ral 2513  df-rex 2514
  Copyright terms: Public domain W3C validator