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

Theorem r19.29 2696
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 2631 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2660 . . 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 2556   E.wrex 2557
This theorem is referenced by:  r19.29r  2697  disjiun  4029  triun  4142  ralxfrd  4564  elrnmptg  4945  fun11iun  5509  fmpt  5697  fliftfun  5827  omabs  6661  findcard3  7116  r1sdom  7462  tcrank  7570  infxpenlem  7657  dfac12k  7789  cfslb2n  7910  cfcoflem  7914  iundom2g  8178  gruiun  8437  supsrlem  8749  axpre-sup  8807  fimaxre3  9719  limsupbnd2  11973  rlimuni  12040  rlimcld2  12068  rlimno1  12143  pgpfac1lem5  15330  ppttop  16760  epttop  16762  tgcnp  16999  lmcnp  17048  1stcrest  17195  txlm  17358  tx1stc  17360  fbfinnfr  17552  fbunfip  17580  filuni  17596  ufileu  17630  fbflim2  17688  flftg  17707  ufilcmp  17743  cnpfcf  17752  tsmsxp  17853  metss  18070  lmmbr  18700  ivthlem2  18828  ivthlem3  18829  dyadmax  18969  r19.29d2r  23197  tpr2rico  23311  esumpcvgval  23461  sigaclcuni  23494  fordisxex  25057  eqfnung2  25221  intopcoaconlem3b  25641  intopcoaconb  25643  unirep  26452  heibor1lem  26636  2r19.29  26823  stoweidlem35  27887  pmapglbx  30580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator