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

Theorem r19.29r 2942
Description: Restricted quantifier version of 19.29r 1705; variation of r19.29 2941. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
r19.29r  |-  ( ( E. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )

Proof of Theorem r19.29r
StepHypRef Expression
1 r19.29 2941 . 2  |-  ( ( A. x  e.  A  ps  /\  E. x  e.  A  ph )  ->  E. x  e.  A  ( ps  /\  ph )
)
2 ancom 448 . 2  |-  ( ( E. x  e.  A  ph 
/\  A. x  e.  A  ps )  <->  ( A. x  e.  A  ps  /\  E. x  e.  A  ph )
)
3 ancom 448 . . 3  |-  ( (
ph  /\  ps )  <->  ( ps  /\  ph )
)
43rexbii 2905 . 2  |-  ( E. x  e.  A  (
ph  /\  ps )  <->  E. x  e.  A  ( ps  /\  ph )
)
51, 2, 43imtr4i 266 1  |-  ( ( E. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  E. x  e.  A  ( ph  /\ 
ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   A.wral 2753   E.wrex 2754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-ral 2758  df-rex 2759
This theorem is referenced by:  r19.29imd  2943  r19.29af2OLD  2945  2reu5  3257  rlimuni  13429  rlimno1  13532  neindisj2  19809  lmss  19984  fclsbas  20706  isfcf  20719  ucnima  20968  metcnp3  21227  cfilucfilOLD  21256  cfilucfil  21257  bndth  21642  ellimc3  22467  lmxrge0  28267  gsumesum  28386  esumcst  28390  esumfsup  28397  voliune  28558  volfiniune  28559  bnj517  29151  cover2  31467  prmunb2  36020
  Copyright terms: Public domain W3C validator