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

Theorem r19.29 2847
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 445 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
21ralimi 2781 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2810 . . 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 2705   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-ral 2710  df-rex 2711
This theorem is referenced by:  r19.29r  2848  r19.29d2r  2853  disjiun  4270  triun  4386  ralxfrd  4494  elrnmptg  5076  fmpt  5852  fliftfun  5992  fun11iun  6526  omabs  7074  findcard3  7543  r1sdom  7969  tcrank  8079  infxpenlem  8168  dfac12k  8304  cfslb2n  8425  cfcoflem  8429  iundom2g  8692  gruiun  8953  supsrlem  9265  axpre-sup  9323  fimaxre3  10266  limsupbnd2  12944  rlimuni  13011  rlimcld2  13039  rlimno1  13114  pgpfac1lem5  16553  ppttop  18452  epttop  18454  tgcnp  18698  lmcnp  18749  bwth  18854  1stcrest  18898  txlm  19062  tx1stc  19064  fbfinnfr  19255  fbunfip  19283  filuni  19299  ufileu  19333  fbflim2  19391  flftg  19410  ufilcmp  19446  cnpfcf  19455  tsmsxp  19570  metss  19924  lmmbr  20610  ivthlem2  20777  ivthlem3  20778  dyadmax  20919  rhmdvdsr  26138  tpr2rico  26195  esumpcvgval  26380  sigaclcuni  26414  voliune  26498  volfiniune  26499  dya2icoseg2  26546  unirep  28447  heibor1lem  28549  2r19.29  28841  stoweidlem35  29673  ralxfrd2  29980  pmapglbx  32983
  Copyright terms: Public domain W3C validator