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

Theorem r19.29 2684
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 2619 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2648 . . 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 2544   E.wrex 2545
This theorem is referenced by:  r19.29r  2685  disjiun  4014  triun  4127  ralxfrd  4547  elrnmptg  4928  fun11iun  5458  fmpt  5642  fliftfun  5772  omabs  6640  findcard3  7095  r1sdom  7441  tcrank  7549  infxpenlem  7636  dfac12k  7768  cfslb2n  7889  cfcoflem  7893  iundom2g  8157  gruiun  8416  supsrlem  8728  axpre-sup  8786  fimaxre3  9698  limsupbnd2  11951  rlimuni  12018  rlimcld2  12046  rlimno1  12121  pgpfac1lem5  15308  ppttop  16738  epttop  16740  tgcnp  16977  lmcnp  17026  1stcrest  17173  txlm  17336  tx1stc  17338  fbfinnfr  17530  fbunfip  17558  filuni  17574  ufileu  17608  fbflim2  17666  flftg  17685  ufilcmp  17721  cnpfcf  17730  tsmsxp  17831  metss  18048  lmmbr  18678  ivthlem2  18806  ivthlem3  18807  dyadmax  18947  fordisxex  24352  eqfnung2  24517  intopcoaconlem3b  24937  intopcoaconb  24939  unirep  25748  heibor1lem  25932  2r19.29  26119  stoweidlem35  27183  pmapglbx  29225
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1530  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator