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

Theorem r19.29 2838
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 2773 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2802 . . 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 2697   E.wrex 2698
This theorem is referenced by:  r19.29r  2839  r19.29d2r  2843  disjiun  4194  triun  4307  ralxfrd  4729  elrnmptg  5112  fun11iun  5687  fmpt  5882  fliftfun  6026  omabs  6882  findcard3  7342  r1sdom  7692  tcrank  7800  infxpenlem  7887  dfac12k  8019  cfslb2n  8140  cfcoflem  8144  iundom2g  8407  gruiun  8666  supsrlem  8978  axpre-sup  9036  fimaxre3  9949  limsupbnd2  12269  rlimuni  12336  rlimcld2  12364  rlimno1  12439  pgpfac1lem5  15629  ppttop  17063  epttop  17065  tgcnp  17309  lmcnp  17360  1stcrest  17508  txlm  17672  tx1stc  17674  fbfinnfr  17865  fbunfip  17893  filuni  17909  ufileu  17943  fbflim2  18001  flftg  18020  ufilcmp  18056  cnpfcf  18065  tsmsxp  18176  metss  18530  lmmbr  19203  ivthlem2  19341  ivthlem3  19342  dyadmax  19482  rhmdvdsr  24248  tpr2rico  24302  esumpcvgval  24460  sigaclcuni  24493  voliune  24577  volfiniune  24578  dya2icoseg2  24620  unirep  26405  heibor1lem  26509  2r19.29  26694  stoweidlem35  27751  ralxfrd2  28059  pmapglbx  30503
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator