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

Theorem r19.29 2656
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 2591 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2620 . . 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 2516   E.wrex 2517
This theorem is referenced by:  r19.29r  2657  disjiun  3973  triun  4086  ralxfrd  4506  elrnmptg  4903  fun11iun  5417  fmpt  5601  fliftfun  5731  omabs  6599  findcard3  7054  r1sdom  7400  tcrank  7508  infxpenlem  7595  dfac12k  7727  cfslb2n  7848  cfcoflem  7852  iundom2g  8116  gruiun  8375  supsrlem  8687  axpre-sup  8745  fimaxre3  9657  limsupbnd2  11908  rlimuni  11975  rlimcld2  12003  rlimno1  12078  pgpfac1lem5  15262  ppttop  16692  epttop  16694  tgcnp  16931  lmcnp  16980  1stcrest  17127  txlm  17290  tx1stc  17292  fbfinnfr  17484  fbunfip  17512  filuni  17528  ufileu  17562  fbflim2  17620  flftg  17639  ufilcmp  17675  cnpfcf  17684  tsmsxp  17785  metss  18002  lmmbr  18632  ivthlem2  18760  ivthlem3  18761  dyadmax  18901  fordisxex  24306  eqfnung2  24471  intopcoaconlem3b  24891  intopcoaconb  24893  unirep  25702  heibor1lem  25886  2r19.29  26073  stoweidlem35  27105  pmapglbx  29109
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 2521  df-rex 2522
  Copyright terms: Public domain W3C validator