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

Theorem reximia 2661
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 10-Feb-1997.)
Hypothesis
Ref Expression
reximia.1  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
reximia  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )

Proof of Theorem reximia
StepHypRef Expression
1 rexim 2660 . 2  |-  ( A. x  e.  A  ( ph  ->  ps )  -> 
( E. x  e.  A  ph  ->  E. x  e.  A  ps )
)
2 reximia.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2mprg 2625 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  reximi  2663  iunpw  4586  tz7.49c  6474  abianfp  6487  fisup2g  7233  unwdomg  7314  trcl  7426  cfsmolem  7912  1idpr  8669  qmulz  10335  zq  10338  xrsupexmnf  10639  xrinfmexpnf  10640  caubnd2  11857  caurcvg  12165  caurcvg2  12166  caucvg  12167  txlm  17358  norm1exi  21845  chrelat2i  22961  xrofsup  23270  esumcvg  23469  wfrlem9  24335  bnj168  29074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator