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

Theorem r19.29 2878
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 447 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21ralimi 2812 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2841 . . 3  |-  ( A. x  e.  A  ( ps  ->  ( ph  /\  ps ) )  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
42, 3syl 16 . 2  |-  ( A. x  e.  A  ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ( ph  /\  ps )
) )
54imp 429 1  |-  ( ( A. x  e.  A  ph 
/\  E. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wral 2736   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-ral 2741  df-rex 2742
This theorem is referenced by:  r19.29r  2879  r19.29d2r  2884  disjiun  4303  triun  4419  ralxfrd  4527  elrnmptg  5110  fmpt  5885  fliftfun  6026  fun11iun  6558  omabs  7107  findcard3  7576  r1sdom  8002  tcrank  8112  infxpenlem  8201  dfac12k  8337  cfslb2n  8458  cfcoflem  8462  iundom2g  8725  gruiun  8987  supsrlem  9299  axpre-sup  9357  fimaxre3  10300  limsupbnd2  12982  rlimuni  13049  rlimcld2  13077  rlimno1  13152  pgpfac1lem5  16602  ppttop  18633  epttop  18635  tgcnp  18879  lmcnp  18930  bwth  19035  1stcrest  19079  txlm  19243  tx1stc  19245  fbfinnfr  19436  fbunfip  19464  filuni  19480  ufileu  19514  fbflim2  19572  flftg  19591  ufilcmp  19627  cnpfcf  19636  tsmsxp  19751  metss  20105  lmmbr  20791  ivthlem2  20958  ivthlem3  20959  dyadmax  21100  rhmdvdsr  26308  tpr2rico  26364  esumpcvgval  26549  sigaclcuni  26583  voliune  26667  volfiniune  26668  dya2icoseg2  26715  unirep  28632  heibor1lem  28734  2r19.29  29025  stoweidlem35  29856  ralxfrd2  30163  pmapglbx  33509
  Copyright terms: Public domain W3C validator