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

Theorem reximia 2648
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 2647 . 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 2612 1  |-  ( E. x  e.  A  ph  ->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  reximi  2650  iunpw  4570  tz7.49c  6458  abianfp  6471  fisup2g  7217  unwdomg  7298  trcl  7410  cfsmolem  7896  1idpr  8653  qmulz  10319  zq  10322  xrsupexmnf  10623  xrinfmexpnf  10624  caubnd2  11841  caurcvg  12149  caurcvg2  12150  caucvg  12151  txlm  17342  norm1exi  21829  chrelat2i  22945  xrofsup  23255  esumcvg  23454  wfrlem9  24264  bnj168  28758
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator