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

Theorem r19.29 2978
Description: Restricted quantifier version of 19.29 1670. See also r19.29r 2979. (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 2836 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2908 . . 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 2793   E.wrex 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-ral 2798  df-rex 2799
This theorem is referenced by:  r19.29r  2979  r19.29d2r  2986  disjiun  4427  triun  4543  ralxfrd  4651  elrnmptg  5242  fmpt  6037  fliftfun  6195  fun11iun  6745  omabs  7298  findcard3  7765  r1sdom  8195  tcrank  8305  infxpenlem  8394  dfac12k  8530  cfslb2n  8651  cfcoflem  8655  iundom2g  8918  supsrlem  9491  axpre-sup  9549  fimaxre3  10499  limsupbnd2  13288  rlimuni  13355  rlimcld2  13383  rlimno1  13458  pgpfac1lem5  17109  ppttop  19486  epttop  19488  tgcnp  19732  lmcnp  19783  bwth  19888  1stcrest  19932  txlm  20127  tx1stc  20129  fbfinnfr  20320  fbunfip  20348  filuni  20364  ufileu  20398  fbflim2  20456  flftg  20475  ufilcmp  20511  cnpfcf  20520  tsmsxp  20635  metss  20989  lmmbr  21675  ivthlem2  21842  ivthlem3  21843  dyadmax  21985  rhmdvdsr  27786  tpr2rico  27872  esumpcvgval  28062  sigaclcuni  28096  voliune  28179  volfiniune  28180  dya2icoseg2  28227  unirep  30179  heibor1lem  30281  2r19.29  30571  stoweidlem35  31771  ralxfrd2  32257  pmapglbx  35368
  Copyright terms: Public domain W3C validator