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

Theorem r19.29 2806
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 435 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21ralimi 2741 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2770 . . 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 419 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 359   A.wral 2666   E.wrex 2667
This theorem is referenced by:  r19.29r  2807  r19.29d2r  2811  disjiun  4162  triun  4275  ralxfrd  4696  elrnmptg  5079  fun11iun  5654  fmpt  5849  fliftfun  5993  omabs  6849  findcard3  7309  r1sdom  7656  tcrank  7764  infxpenlem  7851  dfac12k  7983  cfslb2n  8104  cfcoflem  8108  iundom2g  8371  gruiun  8630  supsrlem  8942  axpre-sup  9000  fimaxre3  9913  limsupbnd2  12232  rlimuni  12299  rlimcld2  12327  rlimno1  12402  pgpfac1lem5  15592  ppttop  17026  epttop  17028  tgcnp  17271  lmcnp  17322  1stcrest  17469  txlm  17633  tx1stc  17635  fbfinnfr  17826  fbunfip  17854  filuni  17870  ufileu  17904  fbflim2  17962  flftg  17981  ufilcmp  18017  cnpfcf  18026  tsmsxp  18137  metss  18491  lmmbr  19164  ivthlem2  19302  ivthlem3  19303  dyadmax  19443  rhmdvdsr  24209  tpr2rico  24263  esumpcvgval  24421  sigaclcuni  24454  voliune  24538  volfiniune  24539  dya2icoseg2  24581  unirep  26304  heibor1lem  26408  2r19.29  26593  stoweidlem35  27651  pmapglbx  30251
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator