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

Theorem r19.29 2997
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 2857 . . 3  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ( ps  ->  ( ph  /\ 
ps ) ) )
3 rexim 2929 . . 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 2814   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  r19.29r  2998  r19.29d2r  3004  disjiun  4437  triun  4553  ralxfrd  4661  elrnmptg  5252  fmpt  6042  fliftfun  6198  fun11iun  6744  omabs  7296  findcard3  7763  r1sdom  8192  tcrank  8302  infxpenlem  8391  dfac12k  8527  cfslb2n  8648  cfcoflem  8652  iundom2g  8915  gruiun  9177  supsrlem  9488  axpre-sup  9546  fimaxre3  10492  limsupbnd2  13269  rlimuni  13336  rlimcld2  13364  rlimno1  13439  pgpfac1lem5  16932  ppttop  19302  epttop  19304  tgcnp  19548  lmcnp  19599  bwth  19704  1stcrest  19748  txlm  19912  tx1stc  19914  fbfinnfr  20105  fbunfip  20133  filuni  20149  ufileu  20183  fbflim2  20241  flftg  20260  ufilcmp  20296  cnpfcf  20305  tsmsxp  20420  metss  20774  lmmbr  21460  ivthlem2  21627  ivthlem3  21628  dyadmax  21770  rhmdvdsr  27499  tpr2rico  27558  esumpcvgval  27752  sigaclcuni  27786  voliune  27869  volfiniune  27870  dya2icoseg2  27917  unirep  29834  heibor1lem  29936  2r19.29  30227  stoweidlem35  31363  ralxfrd2  31798  pmapglbx  34583
  Copyright terms: Public domain W3C validator